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/

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.