Experimental Data for Model Checking C++03 Programs

Citation Author(s):
R. Monteiro
Federal University of Amazonas
R. Gadelha
SIDIA Instituto de Ciência e Tecnologia
C. Cordeiro
University of Manchester
Submitted by:
Felipe Monteiro
Last updated:
Wed, 09/11/2019 - 12:14
Data Format:
0 ratings - Please login to submit your rating.


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.


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


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