We are hiring new student research assistants and tutors. Apply now!
Paper accepted at CCS 2023: Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications

Daniel Baier

Picture of Daniel Baier

Software and Computational Systems Lab
Department of Computer Science
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538 Munich (Germany)

Room F 012, Oettingenstr. 67
Office Hours
By appointment

Thesis Mentoring

Currently assigned topics
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

Interpolants build from an arbitrary SMT solver (develop a layer into JavaSMT to get (tree) interpolants without explicit support of the solver e.g. from proofs or unsat cores) [1, 2, 3, 4]

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.


Publications, Theses, and Projects