Software and Computational Systems Lab

CPAchecker has several different implementations of pointer-aliasing analyses with different levels of abstraction, but no way of inferring information about a programs memory-image, as well as a memory-safety analysis, that tracks the memory image of a program precisely. The goal of this thesis is to create a new CPA based on our memory-safety analysis, which is capable of tracking the abstract or precise memory-image of a program, and inferring pointer aliasing information from the tracked memory. This new CPA is based on the existing Symbolic-Memory-Graph (SMG) analysis, but is meant to be interprocedural, i.e. other analyses in CPAchecker should be able to use it. Therefore, this new CPA needs to be fast and be able to track memory-information based on the information provided by the chosen composite analysis. Automatic tests and an evaluation of this addition to CPAchecker are a necessary part of this thesis.

Java does not offer advanced data-structures like union-find, persistent data-structures with efficient copy operations, or efficient self-balancing trees natively. However, these, and many more, can be useful in situations with the need for specialized data-structures, like in the software verification framework CPAchecker. This project/thesis aims at analyzing where such data-structures would be useful in CPAchecker and then implementing them in Java in the SoSy-Commons library. New data-structures should be automatically tested and documented thoroughly. The efficiency is then to be benchmarked and evaluated.

JavaSMT is a library offering a common interface for many SMT solvers. However, as it is written in Java, it uses the Java Virtual Machine, which invokes a run-time overhead when started. This problem can be reduced by compiling JavaSMT natively, e.g. using Graal-VM. Since this problem is only of concern for non-Java based applications, a Python interface can be added using Graal-VM, which allows the usage of JavaSMT through Python. This can then be evaluated, for example using the setup and benchmark tasks of SMT-COMP.

JavaSMT is a framework that provides a common API for several SMT solvers. Adding support for an additional SMT solver is straightforward. However, JavaSMT is written in Java, while most solvers are written in C or C++. This means one usually has to write bindings using the Java Native Interface. Alternativly, CHC solvers based on SMT solvers could also be added in the existing infrastructure. This topic is suited for a bachelor's thesis.

JavaSMT is a framework that provides a common API for several SMT solvers. These have different strengths and weaknesses. To boost these, common simplification or optimization techniques could be added to boost existingt solvers capabilities. This can be based on solver independent techniques, finding optimal solver settings, or utilizing features from distinct solvers to the currently used etc. This should also be added in the existing infrastructure, including automatic tests, documentation and a thorough evaluation.