Deductive Verification of Java programs with Algebraic Modeling and Multi-Prover Backend: the Why/Krakatoa platform.

Claude Marché

We present the Why/Krakatoa approach to deductive verification of Java programs. Functional behaviors are given in the Java source code, as annotations a la JML. Models can be given using algebraic-style specifications. Verification conditions are generated, whose validity ensures the correctness of source code with respect to the specifications. These are standard first-order formulas, which can be sent to several provers, both interactive ones like Coq or PVS, and automatic ones like Simplify, Yices, or Ergo.


Invited talk at FOOL/WOOD; Saturday, 20 January 2007; Nice, France