Verifiers that can prove programs correct against their full functional specification require, for programs with loops, additional annotations in the form of loop invariants—properties that hold for every iteration of a loop. We show that significant loop invariant candidates can be generated by systematically mutating postconditions; then, dynamic checking (based on automatically generated tests) weeds out invalid candidates, and static checking selects provably valid ones. We present a framework that automatically applies these techniques in support to a program prover, paving the way for fully automatic verification without manually written loop invariants: Applied to 28 methods (including 39 different loops) from various java.util classes, our Dynamate prototype automatically discharged 90% of all proof obligations, resulting in automatic complete correctness proofs of 25 out of the 28 methods—thus outperforming other state-of-the-art tools for fully automatic verification.
The current DynaMate prototype integrates the EvoSuite test case generator, the Daikon invariant detector and the ESC/Java2 static verifier,as well as our gin-dyn technique to dynamically detect loop invariants based on syntactically mutating postconditions.
- Download the DynaMate tool (includes the EvoSuite test case generator, the Daikon invariant detector and the ESC/Java2 static verifier, as well as an implementation of our gin-dyn technique for loop invariant detection).
- Download the data to recreate the DynaMate case study
- Download the data used for the comparison between DynaMate and
- Python Versions 2.7 and 3.2
- ANTLR Python runtime 3.4 (Download)
- Java Development Kits (JDK) Versions 1.5 and 1.6
- Apache Ant Version 1.8.2 (or higher) (Apache website)
- Extract compressed tool downloaded from here
- Extract compressed case study downloaded from here
- Create makefile using python script
python3.2 scripts/create_makefile.py path/to/jdk1.5 path/to/jdk1.6 path/to/dynamate-casestudy 1
- Executing DynaMate on entire case study
- Executing DynaMate on a particular target method
- Check the README file for a list of available target methods in the case study.