Unbounded Heap Support for CPAchecker's Predicate Analysis Using SMT Arrays

— Supplementary Web Page —


Bachelor Thesis in Computer Science at the Chair for Software Systems at the University of Passau


This work introduces a formal definition of a formula converter—the component of a Predicate Analysis that creates SMT formulae for program statements. We use this definition to implement a formula converter that uses the SMT theory of arrays to model the program’s heap accesses. To evaluate this approach, we implemented the formula converter in CPAchecker and ran it with four different SMT solvers: MathSAT5, Princess, SMTInterpol, and Z3. Overall, our converter can prove less programs than the existing uninterpreted functions formula converter due to the higher complexity of solving array formulae, but it can prove more programs with larger array sizes.

You can download the PDF version of the thesis in a black and white version (only has some color on data plots and code listings) or in a colored version (color on every page).

Supplementary Data

In order to get all data created by the benchmarks you can download this data as a bzip2 archive (262MB)

The tables for the different benchmark sets of the SV-COMP suite have been created with the tool BenchExec.

The customized files of the ArraysReach set can be found on a seperate Github repository.