Experimental Data for Model Checking C++03 Programs

Experimental Data for Model Checking C++03 Programs

Citation Author(s):
Felipe
R. Monteiro
Federal University of Amazonas
Mikhail
R. Gadelha
SIDIA Instituto de Ciência e Tecnologia
Lucas
C. Cordeiro
University of Manchester
Submitted by:
Felipe Monteiro
Last updated:
Wed, 09/11/2019 - 12:14
DOI:
10.21227/h44f-fp94
Data Format:
Links:
License:
Dataset Views:
57
Share / Embed Cite
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.

Instructions: 

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

 

* http://esbmc.org/

 

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

Dataset Files

You must be an IEEE Dataport Subscriber to access these files. Login or subscribe now. Sign up to be a Beta Tester and receive a coupon code for a free subscription to IEEE DataPort!

Documentation

AttachmentSize
Binary Data README.md3.08 KB

Embed this dataset on another website

Copy and paste the HTML code below to embed your dataset:

Share via email or social media

Click the buttons below:

facebooktwittermailshare
[1] Felipe R. Monteiro, Mikhail R. Gadelha, Lucas C. Cordeiro, "Experimental Data for Model Checking C++03 Programs", IEEE Dataport, 2019. [Online]. Available: http://dx.doi.org/10.21227/h44f-fp94. Accessed: Sep. 18, 2019.
@data{h44f-fp94-19,
doi = {10.21227/h44f-fp94},
url = {http://dx.doi.org/10.21227/h44f-fp94},
author = {Felipe R. Monteiro; Mikhail R. Gadelha; Lucas C. Cordeiro },
publisher = {IEEE Dataport},
title = {Experimental Data for Model Checking C++03 Programs},
year = {2019} }
TY - DATA
T1 - Experimental Data for Model Checking C++03 Programs
AU - Felipe R. Monteiro; Mikhail R. Gadelha; Lucas C. Cordeiro
PY - 2019
PB - IEEE Dataport
UR - 10.21227/h44f-fp94
ER -
Felipe R. Monteiro, Mikhail R. Gadelha, Lucas C. Cordeiro. (2019). Experimental Data for Model Checking C++03 Programs. IEEE Dataport. http://dx.doi.org/10.21227/h44f-fp94
Felipe R. Monteiro, Mikhail R. Gadelha, Lucas C. Cordeiro, 2019. Experimental Data for Model Checking C++03 Programs. Available at: http://dx.doi.org/10.21227/h44f-fp94.
Felipe R. Monteiro, Mikhail R. Gadelha, Lucas C. Cordeiro. (2019). "Experimental Data for Model Checking C++03 Programs." Web.
1. Felipe R. Monteiro, Mikhail R. Gadelha, Lucas C. Cordeiro. Experimental Data for Model Checking C++03 Programs [Internet]. IEEE Dataport; 2019. Available from : http://dx.doi.org/10.21227/h44f-fp94
Felipe R. Monteiro, Mikhail R. Gadelha, Lucas C. Cordeiro. "Experimental Data for Model Checking C++03 Programs." doi: 10.21227/h44f-fp94