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).

To improve replicability of results, it would be good if our benchmarking framework BenchExec would store as much information as possible about each executed benchmarking run, for example hashes of the respective input files (#418). For this we need code that generates SWHIDs, which could even be developed as a separate library. Afterwards, we also need a way for providing this information to users, e.g., together with #524.