In this page you can find more information about the paper titled: "Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds".

Reproducing the experiments

Tight field bounds computation using the bottom-up tool

Requirements:

• Python 2.7

• Linux OS (it should run well on MacOS, but this was not tested)

To reproduce the experiments about computing tight field bounds download the tool from the link below:

bottomup.tar.gz

Read the included README.txt file for instructions about installing and running the tool.

Data structure analysis using CBMC

Requirements:

• Linux operating system (we did not test the tools on MacOS, but they should work fine)

• CBMC (we employed version 5.2 x64)

To reproduce this set of experiments download the following file, uncompress it, and follow the instructions in the README.txt file.

cbmc-experiments.tar.gz