Benchmarks and tool binaries

This page presents the evaluation results of  the "Synergy" project for benchmarks described in Ku K., Hart T.E., Chechik M., Lie D.: A buffer overflow benchmark for software model checkers. ASE 2007: 389-392. This test suite is from http://www.cs.toronto.edu/~kelvin/benchmark/

• WP.tar.bz (331KB)
• NewST.tar.bz (304KB)
• NewSP.tar.bz (289KB)
• NewST_NewSP.tar.bz (287KB)
• SATQE.tar.bz (257 KB)

The extracted statistics  in one spreadsheet (31KB)

Tool binary with NewST and NewSP techniques.

Command-line parameters to use new techniques:

• For NewST: --refiner pp-wp
• For NewSP: --abstractor ppsatqe

The web-page of the evaluation framework  where original program and installation instructions can be found. To compile C programs into binaries we used goto-cc.