The ESC/Java2 Calculi and Object Logics
Implications on Specification and Verification
ESC/Java2 is an extended static checker for Java. It statically analyses JML-annotated Java program code and finds many common programming errors. ESC/Java2 uses two calculi to generate verification conditions in an object logic that is expressed in the syntax and semantics of the automatic theorem prover Simplify. This talk discusses ESC/Java2, its architecture, problems with the current theory and design, and ongoing work to introduce new logics and calculi for more robust, reliable, and performant ESC using (possibly multiple) theorem provers.