We are hiring new student research assistants and tutors. Apply now!
4 papers accepted at SPIN 2024!

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

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

Teaching

Publications, Theses, and Projects