Software and Computational Systems Lab

CPAchecker has several different implementations of pointer-aliasing analyses, and the current state of what they support is unclear. This leads to the fact that they are rarely used and causes wrong results in case of pointer aliasing. The goal of this thesis is to create a strong CPA for pointer aliasing (either by merging the existing CPAs or rewriting them) that supports all necessary use cases (fast and imprecise as well as more precise) and migrate all existing uses of other pointer CPAs, such that the old code can be deleted (#358). Afterwards, it may be possible to add additional features (e.g., #742) or extend other components of CPAchecker to make use of the new CPA (e.g., #527, #398).

CPAchecker currently models a program's heap as arrays of ints/floats/etc., depending on the types used in the program (cf. Section 4.4.3 of [3]). This is imprecise and prevents us from supporting functions like memset, which treat memory as an array of bytes. The goal of this project is to add an alternative heap encoding to CPAchecker's predicate analysis that allows byte-wise access to the heap and support for memset/memcpy/etc.

Our benchmarking framework BenchExec uses cgroups in order to limit and measure time and memory usage during benchmarking. The Linux kernel is replacing cgroups with a new API (v2) and we need to support this in BenchExec (#133). Once we have it, we can use cgroup namespaces to better isolate our containers and provide full support for nested containers (#436).