"Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds" paper homepage
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
Reproducing the experiments
Tight field bounds computation using the bottom-up tool
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:
Read the included README.txt file for instructions about installing and running the tool.
Data structure analysis using CBMC
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.