About DynaMate


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.

Downloads

  • 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

Requirements

Installation

  1. Extract compressed tool downloaded from here
    2. unzip dynamate.zip
  2. Extract compressed case study downloaded from here
    3. unzip dynamate-casestudy.zip
  3. Create makefile using python script
    4. cd path/to/dynamate
    python3.2 scripts/create_makefile.py path/to/jdk1.5 path/to/jdk1.6 path/to/dynamate-casestudy 1

Excuting DynaMate

  • Executing DynaMate on entire case study
    • make openjdk
  • Executing DynaMate on a particular target method
    • make {method}
  • Check the README file for a list of available target methods in the case study.