Experimental Data for Model Checking C++03 Programs

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