Software and Computational Systems Lab
Institute for Informatics
Ludwig-Maximilians-Universität München (LMU Munich)
80538 Munich (Germany)
- Room F 009, Oettingenstr. 67
- +49 (89) 2180-9182
Please send me encrypted mails!
My GPG key: 0xACCD6DC1
Fingerprint: 8C88 203A 21B7 5B34 78E3 DAFB 4D6D 84D3 ACCD 6DC1
Formal methods use SMT solvers extensively for deciding formula satisfiability. However, solvers may contain critical bugs that lead to unsound results. We can use tools for mutation-based fuzzing on our own API and the underlying SMT solvers. We can report bugs back to the developers and update JavaSMT with fixed solver libraries or bindings.
Currently assigned topics
CWE-Ids for Software Analysis in CPAchecker and SV-COMP (subtopic from 'Real-World Requirements for Software Analysis') [1, 2, 3, 4, 5, 6, 7]
The long description of the supertopic can be found under 'Real-World Requirements for Software Analysis'.
This subtopic is a specialization for finding and documenting CWE-Ids that match them against CPAchecker's analyses. The target is not as broad as the supertopic, but more related to our own software project. Plan:
- Which CWE-Ids are supported by CPAchecker? Can we simply extend CPAchecker for a few more?
- Can we describe CWE-Ids with a specification like the BLAST query language?
- Does SV-COMP provide tasks for the found CWE-Ids?
- Provide a nice overview (webpage?) for those CWE-Ids?
JavaSMT: integrate a new solver (with automated tests and build documentation). Possible candidates:
CVC4, Boolector, OpenSMT, STP, Yices,...
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
Implementing a fast SMT Solver based on interval-computation 
An SMT formula is a boolean formula that includes numbers and common arithmetic operations. Since formal verification techniques often use SMT formulas to represent programs and models , the speed of solving SMT formulas is a very important aspect of formal verification. Studies show that SMT formulas that are created by model checkers or symbolic execution often have a specific structure: The relation between program variables (e.g., "x == y + z") is dependent on program constraints over these variables that only contain a single variable each, e.g., x > 0, y > 0, and z > 10. This example would be represented as the SMT formula x == y + z ∧ x > 0 ∧ y > 0 ∧ z > 10.
The satisfiability of SMT formulas with this specific structure can be computed through the following decision procedure:
1. For each program variable in the formula, compute the interval(s) of possible values for this variable for which the constraints of this variable are satisfied, and
2. Check whether the relations between program variables can be satisfied with the computed intervals.
The goal of this topic is to implement this procedure and to make it available as a Java library. Work on this in the symbolic execution engine Klee has shown great potential, leading to speedups of up to 55x compared to the use of existing complete SMT solvers.
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 & Organization
- WS 2019/20: Softwaretechnik (Übung)
- WS 2019/20: Formale Sprachen und Komplexität (Moodle und Übung)
- WS 2019/20: Softwaretechnik (Übung)
- SS 2019: Praktikum "SEP: Java-Programmierung"
- WS 2018/19: Softwaretechnik (Übung)
- SS 2018: Praktikum "SEP: Java-Programmierung"
- WS 2017/18: Softwaretechnik (Übung)
- SS 2017: SWEP
University of Passau:
- WS 2016/17: Programmierung 2 (Übung)
- SS 2016: Software Engineering (Übung), Sommercamp Informatik
- WS 2015/16: Programmierung 2 (Übung), Entwurfsautomatisierung (Übung)
- Evaluation of Tools at the Competitions on Software Verification 2012, 2013, 2014, and 2015
Publications, Presentations, and Co (List at SoSy-Lab, List at DBLP)
- ESEC/FSE 2020: Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization
- ISoLA 2020: Violation Witnesses and Result Validation for Multi-Threaded Programs, pdf, supplementary website
- ISoLA 2018: In-Place vs. Copy-on-Write CEGAR Refinement for Block Summarization with Caching, pdf, slides, supplementary website
- CPA 2018: Domain-Independent Multi-threaded Software Model Checking, slides
- ASE 2018: Domain-Independent Multi-threaded Software Model Checking, pdf, supplementary website
- AVM 2017: Block-Abstraction Memoization with CEGAR (In-Place vs. Copy-On-Write Refinement), poster
- CPA 2017: Block Abstraction Memoization with Copy-On-Write Refinement, slides
- TACAS 2017: CPAchecker for Reachability, Memory Safety, Overflows, Concurrency, and Termination (Competition Contribution), poster
- TACAS 2017: CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution), doi
- MEMICS 2016: A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker, doi, pdf
- CPA 2016: A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker, slides
- RERS 2016: Gold medal in Reachability Plain and silver medal in Reachability Arithmetic, results
- VSTTE 2016: JavaSMT: A Unified Interface for SMT Solvers in Java, doi, project
- TACAS 2016: CPA-BAM: Block-Abstraction Memoization in CPAchecker (Competition Contribution), doi, pdf, slides
- Master's Thesis 2015: Block-Abstraction Memoization as an Approach to Verify Recursive Procedures, pdf
- HVC 2013: Domain Types: Abstract-Domain Selection Based on Variable Usage, doi, pdf
- Bachelor's Thesis 2012: Ein typbasierter Ansatz zur Kombination verschiedener Verifikationstechniken, pdf