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.