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:
116
Rating:
0
0 ratings - Please login to submit your rating.
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

Thank you for rating this dataset!

Please share additional details of your rating with the IEEE DataPort community by adding a comment.

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: Jun. 03, 2020.
@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