Software and Computational Systems Lab
Department of Computer Science
Ludwig-Maximilians-Universität München (LMU Munich)
80538 Munich (Germany)
- Room F 012, Oettingenstr. 67
- Office Hours
- By appointment
Concurrent Memory Analysis using Symbolic Memory Graphs
CPAchecker offers verification algorithms for concurrent programs without (heap-)memory and non-concurrent programs with (heap-)memory. The goal is to combine these algorithms using a composite analysis, reusing the already existing components. This is then implemented in CPAchecker and evaluated against other verification approaches over the SV-COMP benchmark set.
Boost Symbolic Memory Graph based Explicit Value Analysis with Numerical Abstract Reasoning
Explicit Value Analysis with Symbolic Memory Graphs (SMGs) can analyse programs, including memory operations, fast and efficient. However, Value Analysis often over-approximates values beyond an already encountered bound. The goal is to combine the existing SMG based Value Analysis with the existing Numerical Abstract Domain (APRON) using a composite analysis, reusing the already existing components. This is then implemented in CPAchecker and evaluated against other verification approaches over the SV-COMP benchmark set.
JavaSMT: integrate a new solver (with automated tests and build documentation). Possible candidates:
Bitwuzla, Vampire, dReal, OpenSMT, STP,...
JavaSMT is a framework that provides a common API for several SMT solvers. Adding support for an additional 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. This topic is suited for a bachelor's thesis
JavaSMT: develop and implement a solver-independent SMT2 String parser/composer (with automated tests and build documentation).
JavaSMT is a framework that provides a common API for several SMT solvers. However, there are solver that do not offer parsing/dumping of formulas in the SMT2 format. The goal of this thesis would be the development and implementation of a new, solver-independent layer in JavaSMT, that enables users to generate SMT2 formulas in String form using the API, but also read arbitrary SMT2 formulas into any of the existing solvers APIs without using the solvers parsing abilities. This topic is suited for a bachelor's thesis
If you're a student interested in writing your thesis at our chair, you should also have a look at our full list of currently available theses.