Datasets
Standard Dataset
Experimental Data for Model Checking C++03 Programs
- Citation Author(s):
- Submitted by:
- Felipe Monteiro
- Last updated:
- Wed, 09/11/2019 - 12:14
- DOI:
- 10.21227/h44f-fp94
- Data Format:
- Links:
- License:
- Categories:
- Keywords:
Abstract
A fully-labeled C++03 program dataset provides a unique resource to evaluate model checkers in respect to language coverage. To tackle modern aspects of the C++ language, a large-scale benchmark dataset includes more than 1,500 C++03-compliant programs, which cover different aspects of the language, including exception handling, templates, inheritance, polymorphism, the standard template library, and object-oriented design.
## Experimental Evaluation
ESBMC implements bounded model checking (BMC) based on satisfiability
modulo theories (SMT) to handle complex features that the C++ programming
language offers, such as templates, sequential and associative containers,
inheritance, polymorphism, and exception handling.
This document has the execution process of ESBMC benchmarks used in the
experimental evaluation submitted to IEEE Access journal, with support to Ubuntu OS 14.04.
#### Dependencies
* `boost` library __v1.43__ or higher
* `clang` __v3.8__
* `g++` __v4.8__ or higher
* `glibc headers` compatible with g++
* `/usr/bin/time` executable
#### Content
This folder contains the benchmarks used in the experimental evaluation of the article as well as the scripts needed to collect the metrics regarding the verification tasks.
* _data_
* _benchmarks_
* _category_
*_suite_
* Each test case folder here contains the _main.cpp_ file (the program itself) and its _test.desc_ and _testllvm.desc_ files (a description of the test case containing additional data, _e.g._, expected result and how to verify it).
* _scripts_
* This folder contains the scripts used to collect the metrics for each verifier.
* _tools_
* This folder contains the _ESBMC_ binary and its libraries (i.e., C++ operational models).
#### Verifiers Availability
The verifiers used in this paper can be found at:
- _CBMC v5.8_ - http://www.cprover.org/cbmc/
- _DIVINE v4.0.22_ - https://divine.fi.muni.cz/download.html
- _ESBMC v2.1_ - http://esbmc.org/binaries/
- _LLBMC v2013.1_ - http://llbmc.org/downloads.html
#### Running ESBMC
###### Installation and Execution
* Copy the `esbmc-v2.1.0-linux-static-64` folder from the `tools` folder to your `$HOME` directory.
* Create a symbolic link to `esbmc-v2.1.0-linux-static-64/libraries` from your `$HOME` directory as follows:
```
cd $HOME
ln -s esbmc/libraries libraries
```
* Add the binary `esbmc` to your `.bashrc` as follows:
```
cd $HOME
vi .bashrc
export PATH=$PATH:$HOME/esbmc-v2.1.0-linux-static-64/bin
source .bashrc
```
* The binary provided in `esbmc-v2.1.0-linux-static-64/bin/` folder is for a 64-bits architecture. We also provide another binary for 32-bits architecture in `tools/esbmc-v2.1.0-linux-static-32`.
#### How to Run the Experiments
1. The user needs to build the verification metrics collector script. This is achieved by running `make` inside the _data/scripts_ folder. When it finishes, the built executable named `verification_metrics` will be available inside the _benchmarks_ folder.
2. Then the user must run the script with the desired verifier. This is achieved by running `./verification_metrics <VERIFIER>` inside the _data/benchmarks_ folder, where `<VERIFIER>` is the verifier to be used in the evaluation, _i.e._, `CBMC`, `DIVINE`, `ESBMC`, or `LLBMC`. If one wants to save the results to a text file for later use, one should append `> <FILENAME>` to the latter command, where `<FILENAME>` is the desired filename.
Obs.: Each verifier needs to be installed in the user's computer and they need to be in _$PATH_.