Dualyzer is a verifier for imperative programs based on static analysis with two distinguishing features. First, Dualyzer is versatile being able to prove program safety, confirm true bugs (not false positives from static analysis) and reason about program termination properties. Second, Dualyzer is both precise and efficient, see comparison below with state-of-the-art tools like Interproc, Blast and VS3.

More details are available in a paper published in the ACM Symposium on Applied Computing (SAC) 2010 (pdf) and an extended version published in the Science of Computer Programming journal (pdf preprint).

Download Dualyzer: link (runs on Linux-x86 with glibc 2.7)

Some examples

Example Results from Interproc Results from Blast Results from VS3 (from paper) Results from Dualyzer
McCarthy's f91 Cannot prove (code) Yes - 72sec (fig 3b) Yes - 0.5sec (code)
Queens - safety of array accesses Cannot prove (code) Cannot prove (code) Yes - 1.4sec (code)
Merge - simple assertion Yes - 80sec (fig 4b) Yes - 2.6sec (code)
Merge sort - safety of array accesses Cannot prove (code) Yes - 4.6sec (code)
Quicksort - safety of array accesses Yes - 28.8sec (code) Yes - 1.5sec (code)
SOR - safety of array accesses Yes - 2.1sec (code) Yes - 3.5sec (code)
LU decomposition - safety of array accesses Yes - 7.2sec (code) Yes - 14.3sec (code)

Sample run for Dualyzer

Command What happens
./imp queens.imp Attempts to verify the assertions from the input file queens.imp. In this case it succeeds! Dualyzer also generates a C program (by default the output file a.c) with runtime instrumentation for those assertions that were not proven.
gcc -w a.c Primitives.c Generates a Linux executable.
./a.out Runs the executable.

The following file is needed for the first step above: Primitives.imp

The following files are needed for the second step above, for compilation of the resulting C program (the output of analysis): Primitives.c, Primitives.h

Pages of related tools