2 Papers accepted at SEFM'20: "Difference Verification with Conditions" and "FRed: Conditional Model Checking via Reducers and Folders"

Thomas Lemberger

Picture of Thomas Lemberger

Software and Computational Systems Lab
Institute for Informatics
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538 Munich (Germany)

Office
Room F 005 New!, Oettingenstr. 67
Phone
+49 89 2180 9178
E-Mail
thomas.lemberger@sosy.ifi.lmu.de

GPG-Key

Please send me encrypted mails!
My GPG key: 0x033DE66F
Fingerprint: BBC4 36E1 F2BA BA4E 8E81 872E 9787 7E1F 033D E66F

Thesis Mentoring

Available topics
Topics on Symbolic Execution [1]

Program testing is an established technique in modern software development, but it is, in most cases, not able to cover all potential program paths. In practice, even incomplete coverage goals like branch coverage are not always fulfilled by hand-written tests. Thus, bugs may go unnoticed. In contrast to this, symbolic execution is a program analysis technique that is able to exhaustively analyze a program by executing a program with symbolic inputs instead of concrete ones. During this symbolic execution, constraints on the symbolic inputs are recorded. These constraints show relations between inputs and can be used to create a test suite that fully meets a given coverage goal.

Theses in this topic are concerned with implementing heuristics or improvements to an existing symbolic execution engine in CPAchecker (implemented in Java).

LLVM Compiler Optimizations for Code Analysis [1, 2]

Experimental evaluation of the effect of compiler optimizations and automatic code transformations of LLVM on formal verification.

Finding causes for bugs in programs [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 one such technique to automatically find potential causes for faulty behavior and present the found causes.

Currently assigned topics
Conversion of counterexamples found by software verifiers into an executable test harness that exposes the bug in the program (prototype exists)
Finding causes for bugs with Distance Metrics [1, 2]

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

Finding causes for bugs with Tarantula [1, 2]

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, 2]

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 code-complexity analysis on the component level on the example of CPAchecker [1, 2, 3]
Finished topics
Application of Software Verification to OpenBSD Network Modules
Hybrid Testcase Generation with CPAchecker [1]
Visualization of computation steps and their results in CPAchecker
Finding causes for bugs with Delta Debugging [1, 2]

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 Delta Debugging.

Finding causes for bugs with Error Invariants and unsat cores [1, 2]

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.

Visualization of verification coverage information in CPAchecker
An IDE plugin for CPAchecker

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:

  1. allow developers to run CPAchecker on their current project,
  2. provide some options for customization (e.g., whether to run CPAchecker locally or in the cloud), and
  3. 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

Projects

Publications