Code analysis tool developed using CPAchecker framework. Generates inductive invariants, proves program safety if a separating inductive invariant is found.

Download and Compile

The tool is embedded inside the open-source CPAchecker framework, download and compilation instruction are described at its website.

Running the Tool

# The program we want to analyze:
$ cat test_program.c
#include<assert.h> // By default, CPAchecker verifies "assert" statements.
int main() {
    int sum = 0;
    for (int i=0; i<10; i++) {
        sum++;
    }
    assert(sum == 10);
    return 0;
}


# From the tool directory
$ ./scripts/cpa.sh -preprocess -policy test_program.c
# The output will state whether the property was verified.
                    
To view the obtained invariants:
# View the invariants in the .dot format.
$ xdot output/ARG.dot
                    

Possible Configurations

The command line switch -policy determines the chosen configuration. There are the following configurations available:

  • -policy-intervals: use only interval templates
  • -policy: default configuration, uses octagon templates
  • -policy-refinement: runs multiple analyses in abstraction-refinement mode

Detailed Results for VMCAI2015 "Code Analysis with Local Policy Iteration" article

Comparison was performed on the Loops sub-category of SV-COMP 2015.