Systems Analysis & Verification
NECLA Verification Benchmarks PDF
NECLA Benchmarks: C++ Programs with C++ specific bugs PDF
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.
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.
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).
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.
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.
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.
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.
8.NECLA Benchmarks: Concurrent Trace Programs in TSG format (necla-cmu-smt)
There are 4 sets of benchmarks that are grouped as follows: cp, atom, bank, and indexer, corresponding to simple to complex concurrent programs (cp), our Linux/Pthreads/C implementation of atomicity violations reported in apache server (atom), bank benchmark (bank), and indexer benchmark (indexer). Each set has concurrent trace programs (CTP) generated from the runs of the corresponding concurrent programs. These are expressed in TSG format as explained in the readme file.
9.NECLA Benchmarks: C++ Programs with Exceptions(cppExceptions.tar.gz)
These benchmark set contains 16 C++ programs that cover various aspects of the exception semantics in C++. These small programs test usage of various C++ exception features in realistic scenarios, some of which are close to some standard C++ collection class usage. In addition to cover C++ exception semantic features, these benchmarks can also be used to check for certain exception-safety guarantees as defined by Stroustrup. The benchmarks range in size from about 40 lines of C++ code to about 460 lines. Each benchmark set contains a number of classes, and a main function that drives the execution as a test harness, and may contain user-defined exceptions.
10.NECLA Benchmarks: Division-by-zero False Alarms(division-by-zero.tar.gz)
This benchmark set contains 5 SIMPLE programs that show commonly used practices that developers use to protect a division-by-zero.
They involve non-convex tests (using for instance disjunctions or the absolute value function), strict inequalities tests, or a combination of both.
They have been extracted from available free C source code (GPL) of various projects.
From these real-life examples, we have extracted (by hand) the tests that lead to false alarms and encoded them in SIMPLE language, which is the input language of the Interproc Analyzer.
11.NECLA Benchmarks: C++ Programs with C++ specific bugs(micro.tar.gz)
This benchmark set consists of 16 C/C++ programs that contain various C/C++ specific bugs. These C/C++ specific bugs are obtained via bugs encountered in real programs and various bug pattern sources, such as Effective C++  and Dark side of C++ . These small programs use STL libraries and certain APIs to implement their functionalities, and misuse of these APIs may cause bugs that can be detected by various bug patterns, which can also be used to test the capabilities of bug detection of bug finding tools. The authors present a new abstract domain called access path clusters for effective aliasing-aware typestate analysis, and a new type of analysis called lifetime dependency analysis which allows us to track precisely the effect of the complicated lifetime semantics of temporary objects in C/C++ . The benchmarks are classified into five types of bugs (container, dependency, lockException, smartptr, and style. Each benchmark program may range in size from about several lines of C++ code to about 50 lines, and may contain one or multiple bugs to be detected by bug checkers.
For more details please read here
We would like to acknowledge the support and assistance of Xusheng Ziao, Naoto Maeda, 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.