About DynaMate

Every large software system has a small set of functions on whose correctness it depends. To prove that such functions conform to their specification, automated provers require loop invariants --properties that hold for every iteration of a loop. DynaMate infers loop invariants by systematically mutating postconditions; dynamic checking based on automatically generated tests weeds out invalid candidates and retains the valid invariants. DynaMate paves the way 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 implementation of the gin-pink technique to dynamically detect loop invariants based on syntactically mutating postconditions.

Downloads

• For convenience, download an Ubuntu virtual-machine image with all required dependencies as well as scripts to run the case study. It requires open-source virtualization software VirtualBox (Version 4.3.2 or above) installed in your system.
• Alternatively, you can install DynaMate in your system following the instructions described here.

Installing virtual-machine for using DynaMate

1. Download the Ubuntu virtual-machine image
2. Unpack the virtual-machine image (tar -zxvf dynamate-vm.tar.gz)
3. Install virtualization software VirtualBox (Version 4.3.2 or above)
4. Open VirtualBox
5. Choose Machine→ Add
6. Select within the unpacked folder file dynamate-vm/dynamate-vm.vbox. This will create a Powered-Off "dynamate-vm" virtual machine.
7. Start the dynamate-vm virtual machine (username: dynamate-user, password: password)

Recommended System Requirements

1. Memory: 4 GB
2. Processor: 1.40 GHz
3. Hard Drive Free Space: 15 GB
4. Operating System: Linux, OS X, Windows

Executing DynaMate on the virtual-machine

1. Start the dynamate-vm virtual machine (username: dynamate-user, password: password)
2. Open a Terminal
3. Change directory to /home/dynamate-user/dynamate ($cd /home/dynamate-user/dynamate)
4. Execute DynaMate using $make methodName (for example, $make binarySearch0)

Interactive Case Study results

Explore the results for the methods in the case study:

• From java3.util3.ArrayDeque
• contains
• removeFirstOccurrence
• removeLastOccurrence
• From java3.util3.ArrayList
• clear
• indexOf
• lastIndexOf
• remove0
• From java3.util3.Arrays
• binarySearch0
• equals0
• fill0
• fill1
• fillInteger0
• fillInteger1
• hashCode0
• hashCodeInteger
• insertionSort1
• merge0
• quicksortPartition
• vecswap
• From java3.util3.Collections
• replaceAll
• sort
• From java3.util3.Vector
• indexOf1
• lastIndexOf1
• removeAllElements
• removeRange0
• setSize

Installing and executing DynaMate sources

• Download the DynaMate tool here (includes the EvoSuite test case generator, the Daikon invariant detector and the ESC/Java2 static verifier, as well as our implementation of the gin-pink technique for loop invariant detection). Please check requirements below and follow the installation guide.

Requirements

• Python Versions 2.7 and 3.2
• Python Version 2.7 (Download Version 2.7)
• Python Version 3.2 (Download Version 3.2)
• ANTLR Python runtime 3.4 (Download)
• Java Development Kits (JDK) Versions 1.5 and 1.6
• Java Development Kit (JDK) Version 1.5 (Download)
• Java Development Kit (JDK) Version 1.6 (Download)
• Apache Ant Version 1.8.2 (or higher) (Apache website)

Installing DynaMate on your system

1. Extract compressed tool downloaded from here
tar -zxvf dynamate.tar.gz
2. Create makefile using python configuration script
cd path/to/dynamate
python3.2 scripts/configure.py path/to/jdk1.5 path/to/jdk1.6 path/to/dynamate/case_studies

Executing DynaMate using makefile

• Executing DynaMate on a particular method
make {method}
• Executing DynaMate on entire case study
make fm2014