Supporting Multiple Theories and Provers in ESC and VC
Updates on Verified Java with regards to GC6 and the Verified
ESC/Java is an extended static checker for Java. It statically analyses JML-annotated Java program code and finds many common programming errors. ESC/Java2 is the latest version of ESC/Java. The ESC/Java2 was initiated while Joe Kiniry was a postdoc in the Security of Systems Group at Radboud University Nijmegen. David Cok is the coauthor of ESC/Java2.
This talk first summarizes the work that went on at Nijmegen under the EU FP5 project VerifiCard, particularly the LOOP verification project and ESC/Java2, and summarizes the new EU FP6 project MOBIUS.
Next, the talk summarizes current work on extended static checking with ESC/Java2, particularly with regards to 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.
Finally, the talk discusses how Nijmegen and University College Dublin can contribute to the goals of GC6 and the Verified Software Repository, particularly the development of the MOBIUS Interactive Verification Environment (IVE), as Joe Kiniry leads the development of the IVE from University College Dublin.