Systems Analysis & Verification

Benchmarks

NECLA Verification Benchmarks PDF

1. 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.
Download the BMC benchmarks.
Please contact Chao Wang for any questions/comments.

2. 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.

3. 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.

4. 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.

5. NECLA Non Linear Benchmarks (necla-real-nl)

Besides some challenging benchmarks, there are some which are generated using our modeling of floating-point programs into a CFG representation with integer and real linear/non-arithmetic operations. The modeling is geared towards analyzing numerical stability properties using a BMC framework. The decision problems correspond to BMC instances at different depths.
Download the non-linear benchmarks 2009.
PLEASE DO NOT RE-DISTRIBUTE without permission of NEC Labs America.
Please contact Malay Ganai or Franjo Ivancic for any questions/comments.

6. NECLA CNF Benchmarks (necla-cnf-bench)

These benchmarks are in DIMACS CNF format. These are obtained from Software model checking of 'C' programs such as network protocol with null pointer de-references checks and mobile with array bound violation checks. These are obtained as bounded model checking (BMC) instances at different unroll depths. Without application-level knowledge these benchmark are quite challenging.
Download the CNF benchmarks 2010.
PLEASE DO NOT RE-DISTRIBUTE without permission of NEC Labs America.
Please contact Malay Ganai for any questions/comments.

7.NECLA Benchmarks: Linear and non-linear decision problems in SMTLIB format (necla-cmu-smt)

There are 4 sets of benchmarks, which are generated using our modeling of floating-point programs into a CFG representation with integer and real linear/non-arithmetic operations. The modeling is geared towards analyzing numerical stability properties of such floating-point programs. Such models are analyzed using a BMC framework. Each benchmark set contains a number of decision problems corresponding to BMC instances at different depths. Note that some benchmarks are generated from programs with floating-point computations that are based on discrete-time simulations of hybrid system models written as C programs.
Download the NECLA Linear and non-linear SMTLIB benchmarks 2010.
PLEASE DO NOT RE-DISTRIBUTE without permission of NEC Labs America.
Please contact Franjo Ivancic for any questions/comments.

Acknowledgements

We would like to acknowledge the support and assistance of Pranav Ashar, Srihari Cadambi, Yuusuke Hashimoto-san, Kenjiroh Ikeda-san, Shinichi Iwasaki-san, Yeting Ge, Himanshu Jain, Fusako Mitsuhashi-san, Akira Mukaiyama-san, Ilya Shlyakhter, Zijiang Yang, and Aleksandr Zaks, as well as NEC's Software Business Promotion Unit and the entire Varvel team at NEC's SWED division during the development of F-Soft.