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

Teaching at LMU

Student Talks at LMU

We regularly host students talks in the context of seminars, projects, and theses. All students and staff are welcome to participate. A list of all upcoming talks can be found in the talk schedule.

Teaching in Summer 2020

Courses:

Seminars:

Training (Praktikum):

Teaching in Past Semesters

Information on courses tought in past semesters can be found on a separate page.

Regularly Offered Courses

Seminars

For all seminars these rules apply.

Important Links

Bachelor and Master Theses

We offer several topics for theses on Bachelor and Master level in our research projects (German).

Click on marked topics (▶) to show a more detailed description.
Currently unavailable or finished topics are also shown, and may give inspiration for own ideas.

Please contact us if you are interested in one of these topics or if you want to propose your own topic that is related to our research projects. You can also have a look at our collection of past student reports and theses to get an impression of what a thesis at our chair could look like.

Topics on Formal Verification and Testing

Available topics
Verification of Timed Automata with BDDs [1]

Timed automata are model of computation that was invented 30 years ago with the goal of modelling not only the sequence of events but also the time of their occurrence. Timed automata are automata with a finite set of control states and clock variables whose values continuously increase over time. The objective of this thesis topic is to construct a basic reachability analysis for timed models.

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

Analysis of a real world software project: What can be specified, analyzed?
Literature survey on benchmark sets for software verification and testing and their usage [1, 2]

very broad description. A possible topic could be:

  1. search benchmarks from tools/frameworks/compilers/conferences
  2. transform benchmarks into SV-benchmark compatible format
  3. evaluate SV-COMP tools on new benchmarks, i.e., perform a case study whether the SV-COMP tools are ready for industry benchmarks

Refinement Selection with Adjustable-Block Encoding [1, 2, 3]
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.

Violation and Correctness Witnesses for Conditional Model Checking [1, 2]
Heuristics for Selecting Predicates for Partial Predicate Abstraction [1]
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.

LTL specifications in deductive verification
Development of an interactive theorem prover for untyped logic
Real-World Requirements for Software Analysis [1, 2, 3, 4, 5, 6]

The National Institute of Standards and Technology (NIST) has published a specification for capabilities that a "Source Code Security Analysis Tool" needs in order to be useful in software security assurance [1][2]. This is accompanied by test suites (subsets of the NIST SARD test suite, e.g. suite 100 and 101 [3]) with programs that have to be checked for certain weaknesses [4][5]. For classification of the weaknesses, CWE-IDs are used.

This now leads to various interesting research questions. A subset of those can be addressed by a project or thesis, depending on the available time and progress.

0. How can the CWE-IDs from the relevant SARD test suites be mapped to the specification that are used in the Competition on Software Verification(SV-COMP)?
Some of the weaknesses, e.g. memory-safety related ones or undefined behavior like overflows, are already checked for in the SV-COMP. For the CWEs that cannot be translated into the specifications currently used in the SV-COMP, a critical discussion should be added on how easy/hard it would be to add these and on how easy/hard it is to check for those properties. The extend of this discussion can be tuned to the scope of the project/thesis.

1. How many of the tests in the test suite can already be checked by the automatic software verifiers that participated in the Competition on Software Verification(SV-COMP)?
One of the claims of the SV-COMP is that it shall reflect real-world problems in software verification. As such, it is of interest to determine whether this is the case by applying the participating tools to tasks that are used in industry, like the SARD test suite.
Provided that the license allows this, the corresponding test cases can be extracted from the relevant SARD test suites and converted into tasks for the SV-COMP. A task in the SV-COMP consists of a program and a specification, so ideally the right specification is automatically determined by parsing the information in the xml manifest of the SARD test suite. After the conversion is complete, an extensive evaluation with the tools that participated in the SV-COMP (and optionally other tools, like the ones listed in [6]) shall be performed.

2. Can CPAchecker be extended (e.g. by new analyses) to find these weaknesses and become a Source Code Security Analyzer like many other tools[6]?
Currently, CPAchecker is not really designed to return multiple findings, as in verification it is usually enough to show one specification violation. For some CWEs there should be support, e.g. memory safety or overflows. Others however (e.g. "CWE-134: Uncontrolled Format String") would require a new analysis to be implemented. For reducing the scope of the thesis/project, one can also just pick a subset of the CWEs and implement the corresponding analysis or analyses. Another way to adapt the scope is to only look at some of the requirements. These are divided into mandatory features SCSA-RM-{1,2,3,4,5,6} and optional features SCSA-RO-{1,2,3}[1].

BTOR2 frontend for CPAchecker [1, 2]
Byte-level heap of predicate analysis CPAchecker [1, 2, 3]

CPAchecker currently models a program's heap as arrays of ints/floats/etc., depending on the types used in the program (cf. Section 4.4.3 of [3]). This is imprecise and prevents us from supporting functions like memset, which treat memory as an array of bytes. The goal of this project is to add an alternative heap encoding to CPAchecker's predicate analysis that allows byte-wise access to the heap and support for memset/memcpy/etc.

Invariant Generation through Sampling [1]

Finding the right invariants is essential when trying to proof properties about programs with loops. In CPAchecker we currently have a search-based analysis that generates candidate invariants. Another approach is to try to learn and continuously refine the invariant by training a classifier. This should work especially well if the neccessary invariants are linear equalities, as this corresponds to the classification boundary of a linear classifier.

Currently assigned topics
Conversion of counterexamples found by software verifiers into an executable test harness that exposes the bug in the program (prototype exists)
Improve analysis of Java programs in CPAchecker
Improve predicate analysis based on domain-type of variables in CPAchecker [1, 2]
Verification Coverage: what parts of a program are covered by a verifier? [1]
Separation Logic in CPAchecker
Non-termination analysis in CPAchecker
Exchangeable format for assumption automata in conditional model checking [1]

Conditional model checking (CMC) [1] is a technique for the combination of different verification approaches, which works as follows. Initially, the first verifier explores a given verification task. In case the first verifier does not finish its exploration, it finally outputs a condition, a description of the explored state space. The output condition is used by the subsequent verifier to restrict its exploration towards the unexplored state space.
The verifier CPAchecker supports the CMC approach. However, the existing CMC implementation uses a tool-dependent condition format, which is only understood by CPAchecker. Furthermore, CPAchecker is currently only able to use its own condition format to restrict the exploration of the state space.
The goal of this thesis is the development of a tool-independent condition exchange format, to integrate this new exchange format into CPAchecker and to practically evaluate it against the existing tool-dependent format. The idea is to use a tool-independent exchange format for the condition, which is similar to the existing exchange formats for correctness and violation witnesses [2,3]. To achieve this goal, one should first identify how the two formats differ theoretically and practically. On this basis, the tool-independent should be developed and integrated in the existing infrastructure for witness exports. To cross-check the realization of the new format, the efficiency and effectivity of CMC when using the existing or the newly developed format should be compared.

Literature:
[1] Dirk Beyer, Thomas A. Henzinger, M. Erkan Keremoglu, and Philipp Wendler. 2012. Conditional model checking: a technique to pass information between verifiers. In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering. ACM, New York, NY, USA, , Article 57 , 11 pages.
[2] Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, and Andreas Stahlbauer. 2015. Witness validation and stepwise testification across software verifiers. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering. ACM, New York, NY, USA, 721-733.
[3] Dirk Beyer, Matthias Dangl, Daniel Dietsch, and Matthias Heizmann. 2016. Correctness witnesses: exchanging verification results between verifiers. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM, New York, NY, USA, 326-337.

Make PCC approach(es) in CPAchecker understand correctness witnesses [1, 2]
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.

Implementation and Evaluation of k-Shrinkability [1, 2, 3, 4]
Information flow testing for PGP keyservers
Implement Fuzzing in CPAchecker
SMT-based checking and synthesis of formal refinements
Frontends for a deductive verifier (Python)
Frontends for a deductive verifier (Boogie)
Guided fuzz testing with stochastic optimization
Interactive verification debugging
A code-complexity analysis on the component level on the example of CPAchecker [1, 2, 3]
Predicate-based Analysis of Concurrent Programs [1, 2, 3]

Issue 464

Finished topics
String analysis in CPAchecker [1, 2]
LTL software model checking
Correctness-witness validation using predicate analysis

Verifiers take a program and a specification as input and output whether the program fulfills the specification.If the answer is yes, the verifier can output additional information in form of a correctness witness.This correctness witness can then be used (e.g. by another verifier) to validate that the answer is correct.Our verifier CPAchecker provides many different analyses for verification, but only one of them (called k-Induction) is currently able to validate witnesses.An analysis based on predicate abstraction already exists in CPAchecker that should be able to validate witnesses with minor to moderate programming effort.Once this is working, predicate abstraction could also give insights into which information is missing in the witness.At the end, an evaluation of the new witness validation can be performed on an already existing set of representative programs using our verification cluster.This topic is suitable for a bachelor's thesis, but could also be extended for a master's thesis on request.

Heuristic selection of verification analyses
A JavaScript frontend for CPAchecker
Support for exceptions in the Java analysis of CPAchecker
Towards understandability of verification result: visualization of graphs produced by verifiers
Predicate analysis based on splitting states for CPAchecker [1, 2]
Application of Software Verification to OpenBSD Network Modules
Unify analyses (ValueAnalysis, IntervalAnalysis, SignAnalysis) in CPAchecker by using a common data-wrapper for numerical values (integers, bitvectors, floats, ...), optional: support for symbolic values, BDDs, and Octagons [1]
Define and evaluate different refinement approaches for interval domain or BDD domain (widening, splitting, interpolation, path prefixes) [1, 2, 3]
Symbolic Memory Graphs in CPAchecker [1, 2]
Multi-process architecture for BAM-parallel to provide cluster-based software analysis, maybe with central or shared database for reached states
Backwards analysis for CPAchecker, initially BDD- and predicate-based (both partially implemented somewhere), later symbolic and explicit analysis.
Good, bad, ugly interpolants. Measure interpolants and build heuristics. Topic might be related to refinement selection. [1]
Hybrid Testcase Generation with CPAchecker [1]
Visualization of computation steps and their results in CPAchecker
Parallel BDDs in Java (cf. Sylvan) [1]
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)

Specifying Loops with Contracts. [1]
Rely/Guarantee Reasoning for Separation Logic in SecC
Loop Contracts for Boogie and Dafny

Topics on Reliable Benchmarking and Measurements

Currently assigned topics
Improve usability of summary tab for HTML tables of BenchExec [1]
Finished topics
Modern architecture and tests for HTML tables of BenchExec [1]
Measuring and optimizing energy consumption of verification work

Topics on SMT Solvers and Java SMT

Available topics
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]
Fuzzing for SMT Solvers on API Level [1, 2]

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
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 [1]

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.

Finished topics
SMT query caching, slicing, and simplification module for Java SMT [1]
BDD support in JavaSMT, e.g. add Regions/RegionManager or even something like Q3B to JavaSMT [1, 2, 3]

JavaSMT is a framework that provides a common API for several SMT solvers. For certain problem types, BDDs can be used as a replacement of SMT solvers, as demonstrated by Q3B. The verifier CPAchecker too contains an abstraction layer (Regions/RegionManager) that enables switching between solver and BDDs, while it uses JavaSMT to be able to switch between different solvers. Ideally, the code can be refactored such that the switching between SMT solver and BDD is moved from CPAchecker to JavaSMT. The goal is NOT to add Q3B to the list of solvers supported by JavaSMT, but rather have our own implementation that takes the Regions/RegionManager of CPAchecker as starting point.

Topics on BDDs, ZDDs and ParallelJBDD

Available topics
Design a ZDD wrapper wich enables the use of ZDDs in CPAchecker [1]
Implement more decision diagrams in ParallelJBDD (chain reduced BDDs/ZDDs, tagged BDDs, ...) [1]
Implementation of optimization techniques in ParallelJBDD (dynamic variable reordering, complementary edges, ...) [1, 2]

Collaboration with Bundeswehr University

We also offer thesis topics in collaboration with the PATCH lab at Bundeswehr University. These theses will be formally supervised by our chair, but the day to day work will be guided by a mentor from the PATCH lab.

The language for the following theses is English.

Currently assigned topics
SV-comp Benchmarks for Weak Memory Models [1, 2]

SV-Comp is the International Competition on Software Verification. It serves as a platform for the research community to evaluate tools targeting verification of C and Java programs. A total of 28 tools from 11 different countries participate in SV-Comp’20.

The simplest (and strongest) model of computation for concurrent programs is sequential consistency (SC), i.e. interleaving semantics. However, for performance reasons, mainstream processors perform optimisations that results in more possible executions than those allowed by SC. This new execution can result in bugs in the program which are hard to detect. All executions which are valid according to a certain processor are specified by its memory model.

We aim to create a new category in SV-Comp dealing with memory models. We currently have a collection of more than twelve thousand benchmarks that were used to validate the formalisation of the memory models of x86, Arm and Power processors and the Linux kernel. Those benchmarks are written in the litmus format, which is only supported by a small number of tools. The goal of this thesis is to port the benchmarks from the litmus format to C code. Dartagnan is a verification tool with support for memory model that can already parse all such benchmarks. What is required, is to implement an exporter from Dartagnan’s intermediate representation of programs to C.

Verification Witnesses: from Llvm to C [1, 2]

Dartagnan is a software verification tool. It takes a C program, it compiles it to Llvm and then it performs the verification on the Llvm code. In 2020, Dartagnan participated for the first time in Sv-Comp, the International Competition on Software Verification. One of the requirements of Sv-Comp, is to provide verification witnesses: a proof of correctness or a counterexample. Dartagnan can already generate a counterexample witness as a graph. However, this graph refers to the Llvm code while Sv-Comp requires to generate a counterexample witness w.r.t to input C program. The information mapping the C instructions with the corresponding Llvm code is provided by the transformation from C to Llvm used by Dartagnan. However it is not currently used. The goal of this thesis is to use this information and convert the counterexamples generated by Dartagnan to witnesses w.r.t the C code, thus fulfilling Sv-Comp requirements.

Tipps

When writing a thesis, follow our thesis guidelines and evaluation criteria and use these technical hints for writing (a paper). The software that we use may also be helpful.