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.

Challenges

• The Longest Repeated Substring challenge deals with structural analysis of a flat data structure (array of characters/ integers). We have added a class Lemmas, which is technically not part of the program, but contains lemmas which were required to close the proof on LRS. Download: [LCP.java] [LRS.java] [SuffixArray.java] [Lemmas.java]
• The Prefix Sum challenge also works with arrays, but performs non-trivial arithmetic in-situ operations on the array. Download: [PrefixSumRec.java]
• The Deletion in a Tree challenge is about inspecting and modifying a non-cyclic linked data structure of binary search trees. Download: [Tree.java]

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.

Documentation

• The definite documentation to these challenges is the paper Implementation-level Verification of Algorithms with KeY to be published in Software Tools for Technology Transfer. [Preprint version]
• The best source on the KeY tool is the book Verification of Object-Oriented Software. The KeY Approach. Please note that the book covers legacy version 1.0 of KeY, while the above files only work with version 2.2 or later. A tutorial for KeY 2.2 is currently in preparation.
• There is a lot of material on learning JML, see this page.

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