Department of Systems Analysis & Verification - BENCHMARKS

NEC Laboratories America, Inc., Princeton Campus

NECLA Verification Benchmarks PDF

NECLA BMC Benchmarks (necla-bmc)

In this directory, there are 8 benchmark examples. The verification models (e.g., "ftp_1.blf") are in the BLIF format. Each model has a corresponding property file (e.g., "ftp_1.prp"), which consists of a set of negated invariant properties. The properties are of the form EF p, where p is a propositional formula. These are useful for finding bugs for invariant properties (AG p) by using BMC.

PLEASE DO NOT RE-DISTRIBUTE without permission from NEC Labs America.

Please contact Chao Wang for any questions/comments.

Download necla-bmc.tar.gz

NECLA SMT Benchmarks (necla-smt)

In this collection, there are 3 main categories of benchmarks in SMT-lib format.

• small_smts.tar: 40 small examples,
  • names listed in file list-small-smt,
  • sat/unsat results reported by yices 1.0 in outfile-small-smt.
• med-smts.tar: 364 medium examples,
  • names listed in file list-med-smt,
  • sat/unsat results reported by yices 1.0 in outfile-med-smt.
• large_smts.tar: 2383 large examples,
  • names listed in file list-large-smt,
  • sat/unsat results could not be obtained.

These SMT benchmarks were generated from SMT-based BMC engine inside F-Soft framework.

PLEASE DO NOT RE-DISTRIBUTE without permission of NEC Labs America.

Please contact Malay Ganai for any questions/comments.

NECLA SAT Benchmarks (necla-sat-ckt)

These benchmarks for SAT are derived from BMC application in NEC's VeriSol verification platform. Each benchmark corresponds to a BMC instance at some unrolled depth. It represents a SAT formula in circuit BLIF format (not CNF).

PLEASE DO NOT RE-DISTRIBUTE without permission of NEC Labs America.

Please contact Malay Ganai for any questions/comments.

NECLA Static Analysis Benchmarks (necla-static-small)

These benchmarks are small C programs that demonstrate common programming situations that arise in practice such as interprocedural dataflow, aliasing, array allocation modes, array size propagation, string library usage and so on. The ability of different static techniques to prove them correct is an indication of their areas of strengths and weaknesses.

Download the small static analysis benchmarks for 2008.

PLEASE DO NOT RE-DISTRIBUTE without permission of NEC Labs America.

Please contact Sriram Sankaranarayanan for any questions/comments.

Acknowledgements

We would like to thank Yeting Ge, Himanshu Jain, Ilya Shlyakhter, Zijiang Yang, and Alex Zaks for their contributions.

Website deisgn by Dragonfly Interactive, LLC