logo

Home




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.

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.


NEC Laboratories America, Inc.
Princeton Campus - 4 Independence Way, Suite 200, Princeton NJ 08540   |    Cupertino Campus - 10080 North Wolfe Road, Suite SW3-350, Cupertino, CA 95014
webmaster@nec-labs.com   ©2008 NEC Laboratories America, Inc. All rights reserved. Please Read our Privacy Policy

Website deisgn by Dragonfly Interactive, LLC