Result Certification of Static Program Analysers with Automated Theorem Provers
Proofs and experiments

Source code

Read the paper and download the Coq development and experiments' results.

Experiments

As indicated on the paper, all tests were done on a laptop running Linux with 4GB memory and Inter Core 2 Duo cpu at 2.93GHz. We used

• Why3 0.80 version, fetched from the webpage of the Why3 project
• Z3 3.2, an executable can be fetched on the webpage of z3 on the microsoft research website, there are no link for the linux binaries on the webpage for now, but the archive is there if the url is known.
• Alt-ergo 0.94, that can be obtain at the webpage of the Alt-Ergo project
• Vampire 0.6, thanks to the Vampire team
• E 1.6, obtained from Stefan Schultz's webpage

The archive of the experiments' results contains a directory "NullPointer" with the null pointer analyser, the VC generateur, and a directory "tests" and a directory "results". The directory tests contains the Java programs (sources and binaries) on which all experiments were done. To compile the analyser and the VC generator, it is necessary to install

• OCaml 3.12, fetchable on the OCaml webpage,
• Javalib and Sawja, the OCaml toolbox used to program the analyser, fetchable from the Sawja webpage.
Once Sawja is installed, use make in the NullPointer directory to build the analyser producing VCs, and type make in the tests directory to generate the VCs in the Why3 format.

To launch the solvers on the VCs, it is necessary to install Why3 0.80, fetchable from the webpage of the Why3 project. The Makefile in the tests directory defines a variable CLASSPATH which must contains the classpath to the standard library.

In the "tests" directory, is a small bash script, "bench.sh", which use Why3 to launch the provers on the files containing the VCs. It is configured so as to launch CVC3, Alt-Ergo, Z3, E and Vampire. It produce on file "result_PRG.txt" for each program PRG and a file "result.txt" synthesizing the results. To use the script to call why3, make sure "bench.sh" is executable, and tape "make bench" is the tests directory. The directory "results" contains the files generated by this script on our system.