Thomas Lemberger

Software and Computational Systems Lab
Department of Computer Science
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538
Munich
(Germany)
- thomas.lemberger@sosy.ifi.lmu.de
- ORCID
-
0000-0003-0291-815X
GPG-Key
Please send me encrypted mails!
My GPG key: 0x033DE66F
Fingerprint: BBC4 36E1 F2BA BA4E 8E81 872E 9787 7E1F 033D E66F
Thesis Mentoring
Finished topics
Mutation based Automatic Program Repair in CPAchecker [1]
Debugging software usually consists of three steps: 1. finding an error in the program, 2. finding the cause for that error (the fault), and 3. fixing that fault. By default, fixing the fault is done manually by a programmer, which often consumes vast amount of resources and may introduce new bugs. To ease that task, this topic is concerned with automatic program repair. After finding a potential fault in a program, automatic program repair proposes fixes and often checks the validity of these fixes. The goal is to implement and evaluate a technique for automatic program repair in C programs in the state-of-the-art verification framework CPAchecker. The complexity of the technique and the scope of the topic is based on the thesis type (project, bachelor or master). Programming is done in Java.
Fault Localization in Model Checking. Implementation and Evaluation of Fault-Localization Techniques with Distance Metrics [1]
There are many different ways to find out whether a program is buggy, for example testing or formal verification. Once we know that a program is buggy, i.e., that it shows some faulty behavior, a developer has to manually debug the program to find the cause of the problem and fix it - this is a difficult and long-taking process. The aim of this thesis is to help programmers with debugging through the use of distance metrics (cf. Explaining Abstract Counterexamples, 2004).
Fault Localization for Formal Verification. An Implementation and Evaluation of Algorithms based on Error Invariants and UNSAT-cores [1]
There are many different ways to find out whether a program is buggy, for example testing or formal verification. Once we know that a program is buggy, i.e., that it shows some faulty behavior, a developer has to manually debug the program to find the cause of the problem and fix it - this is a difficult and long-taking process. The aim of this thesis is to help programmers with debugging by implementing Error Invariants and bug-finding with unsat cores, techniques for bug-finding based on boolean representations of the faulty program, to (1) automatically find potential causes for faulty behavior and (2) present the found causes.
Test-based Fault Localization in the Context of Formal Verification: Implementation and Evaluation of the Tarantula Algorithm in CPAchecker [1]
There are many different ways to find out whether a program is buggy, for example testing or formal verification. Once we know that a program is buggy, i.e., that it shows some faulty behavior, a developer has to manually debug the program to find the cause of the problem and fix it - this is a difficult and long-taking process. The aim of this thesis is to help programmers with debugging by implementing Tarantula, a technique for bug-finding based on test coverage, to (1) automatically find potential causes for faulty behavior and (2) present the found causes.
Converting Test Goals to Condition Automata [1]
Conditional Model Checking and Conditional Testing are two techniques for the combination of respective verification tools. Conditional Testing describes work done through a set of covered test goals and Conditional Model Checking describes work done through condition automata. Because of this discrepancy, the two techniques can not be combined. To bridge this gap, this thesis transforms a set of test goals into a condition automaton to allow easy cooperation between Conditional Testing and Conditional Model Checking.
A Language Server and IDE Plugin for CPAchecker [1]
At the moment, there are two ways to use CPAchecker: Locally through the command-line, and in the cloud through a web interface. Both options require C developers to leave their IDE everytime they want to run CPAchecker, which disrupts their workflow. The goal of this project is to build an IDE plugin that provides a seamless experience of using CPAchecker (e.g., for Eclipse CDT, VisualStudio Code or mbeddr). We would like the plugin to focus on ease of use and immediate feedback that is easy to comprehend. The plugin should:
- allow developers to run CPAchecker on their current project,
- provide some options for customization (e.g., whether to run CPAchecker locally or in the cloud), and
- provide useful feedback (e.g., if a possibly failing assert-Statement was found by CPAchecker)
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
- SS'22: Seminar Machine Learning in Software Engineering
- SS'22: Science and Practice in Software Engineering
- SS'22: Testen (Blockveranstaltung)
- WS'21: Semantics of Programming Languages (Blockveranstaltung)
- WS'21: Training Course (Praktikum) "Planmäßige Entwicklung eines größeren Softwaresystems"
- SS'21: Training Course (Praktikum) "SEP: Java-Programmierung"
- SS'21: Testen (Blockveranstaltung)
- WS'20: Semantics of Programming Languages (Blockveranstaltung)
- WS'20: Software Verification
- WS'20: Seminar Software Quality Assurance
- WS'20: Testen (Blockveranstaltung)
- SS'20: Theoretische Informatik für Medieninformatik
- WS'19/20: Training Course (Praktikum) "SEP: Java-Programmierung"
- SS'19: Testen (Blockveranstaltung)
- SS'19: Training Course (Praktikum) on "Advanced Software Engineering"
- WS'18/19: Training Course (Praktikum) "SEP: Java-Programmierung"
- SS'18: Training Course (Praktikum) on "Advanced Software Engineering"
- WS'17/18: Formal Specification and Verification 2
- WS'17/18: Training Course (Praktikum) on "Formal Specification and Verification 2"
Projects
- TestCov: Robust Test Execution, Coverage Measurement, and Test-suite Reduction (Maintainer)
- CondTest: A Proof of Concept for Conditional Software Testing (Creator)
- LLVM-j: Java Bindings for LLVM Libraries (Maintainer)
- CPAchecker: The Configurable Software-Verification Platform (Contributor)
- BenchExec: A Framework for Reliable Benchmarking and Resource Measurement (Contributor)