We are hiring new student research assistants and tutors. Apply now!
Paper accepted at ICSE 2023: "CoVeriTeam Service: Verification as a Service"

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)

Office
Room F 012, Oettingenstr. 67
E-Mail
firstname.lastname@sosy.ifi.lmu.de
Office Hours
By appointment
ORCID
0000-0001-9116-1974

Thesis Mentoring

Available topics
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

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]
Implement more decision diagrams in ParallelJBDD: Algebraic Decision Diagrams (ADD) [1]
Optimize ParallelJBDD (e.g. Chain Reduction or other techniques) [1, 2]

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.

Teaching

Publications, Theses, and Projects