Domagoj Babic

Domagoj Babic

Sw Verification Benchmarks

Benchmarks generated by the Calysto static checker.

Description:

Benchmarks available on this page are generated by the Calysto static checker, and correspond to *-sensitive checking of NULL pointer dereferencing.

 

Logic:

Benchmarks are modular arithmetic constraints, with rich Boolean structure.

 

Structure:

The benchmarks should contain little or no structural redundancies. Calysto performs exhaustive common sub-expression elimination, effectively breaking structural symmetry. Operations with constants (like a*1) are already simplified away.

 

Versions:

Verification conditions (and therefore benchmarks as well) change each time I modify Calysto, improve its powerful expression simplifier, discover that something works better in my setting,... These changes are inevitable. So, to make sure that comparisons of different solvers on my benchmarks are meaningful, benchmarks will be versioned as Calysto releases. So, benchmark set X_v1.6 corresponds to Calysto release 1.6. The sets will be re-generated only when I deem that the new set is sufficiently different from the older one. Due to limited disk space, I will not be able to keep the older versions.

 

Outline:

 

This page contains benchmarks generated by Calysto v1.3 in the SF format. Other formats can be easily generated:

* Dimacs CNF - run Spear with --sf2cnf

* SMT QF_BV - use sf2smt Spear tool