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)
| 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) |
| 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