KeY solutions to the verification competition at FM 2012

On this page, you may find the solutions by the KeY team at the verification competition at FM 2012 held on August, 30th and 31st 2012 in Paris. The team consisted of Daniel Bruns and Wojciech Mostowski.

All solutions are implemented in Java and specified with the Java Modeling Language (JML). The source files can be compiled with Java 1.4 or later. If you would like to run them, please add respective main() methods. Proofs have been done using the KeY tool, which is a software verification tool for Java with a dedicated interactive theorem prover for first-order dynamic logic. To load the solutions requires KeY version 2.2 or later. The solutions may not be usable with other JML tools (e.g., runtime checkers) because of KeY-specific extensions.


All solutions are shipped with KeY. You can find the files under the paths "examples/heap/fm12_*" in the KeY main directory. KeY 2.4 features a new example browser: select "load example" in the main window and look out for FM12.


Last addition to this page: 2015-01-09 10:34 CET