Abstract:
|
ESC/Java2, a static analyser for Java code has been written between 1996 and 1999 by Compaq. At that time the only efficient prover was Simplify, that's why ESC/Java2 was entirely relying on it. With the arrival of new provers and the satisfiability modulo theory (SMT) standard, there was an opportunity to benefit of the lastet advances in that area. It raised problems related to logic (need for new many-sorted logics) and generic design (how to handle different provers easily). |