The DFG research training group ConVeY started on July 1st.

Teaching at LMU

Teaching in Summer 2019

Courses:

Seminars:

Training (Praktikum):

Teaching in Winter 2018/19

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

Support for exceptions in the Java analysis of CPAchecker
Software Model Checking based on automata for CPAchecker [1]
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]
Multi-process architecture for BAM-parallel to provide cluster-based software analysis, maybe with central or shared database for reached states
Experimental evaluation of the effect of pre-processing on analyses (e.g., predicate analysis). Pre-processing (e.g., loop mutations, constant propagation, slicing) can happen in the compiler (gcc, cil, LLVM) or the intermediate representation (CFA). Topic may be related to good, bad, ugly interpolants.
Make PCC approach(es) in CPAchecker understand correctness witnesses [1, 2]
Violation and Correctness Witnesses for Conditional Model Checking [1, 2]
Heuristics for Selecting Predicates for Partial Predicate Abstraction [1]
Fault Localization in Error Traces with Error Invariants and UNSAT Cores [1]
SMT Solving through Computation of Satisfying Multi-Intervals [1]

Studies show that SMT formulas that are created by model checkers [2] or symbolic execution [3] often have a specific structure: The relation between program variables (e.g., "x == y + z") is dependent on multiple constraints over these variables that each only contain a single variable (e.g., "x > 0", "y > 0", "z > 10", "z < 20"). An example for such a formula would be "x == y + z \land x > 0 \land y > 0 \land z > 10 \land z < 20".
The goal of this work is to implement an (incomplete) SMT solving routine that tries to exploit this specific structure through the following process:
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.
Work on this [1] that is implemented in the symbolic execution engine Klee [4] has shown great potential, leading to speedups of up to 55x.

[1]: http://srg.doc.ic.ac.uk/files/papers/parti-ase-18.pdf
[2]: https://mitpress.mit.edu/books/model-checking
[3]: https://www.cs.umd.edu/class/fall2014/cmsc631/papers/king-symbolic-execution.pdf
[4]: https://klee.github.io

Implementation and Evaluation of "Software Model Checking for People Who Love Automata" (the Automizer algorithm) [1]
Visualization of test and verification coverage information in graph-shape visualizations
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)

Specification languages for deductive verification
Reasoning and interaction patterns of proof assistants - survey, description, experiments, and improvements.
Assigned/Finished Topics
String analysis in CPAchecker [1, 2]
LTL software model checking
Conversion of counterexamples found by software verifiers into an executable test harness that exposes the bug in the program (prototype exists)
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
Towards understandability of verification result: visualization of graphs produced by verifiers
Predicate analysis based on splitting states for CPAchecker [1, 2]
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]
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]
Separation Logic in CPAchecker
Symbolic Memory Graphs in CPAchecker [1, 2]
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]
Automatic test case generation based on Symbolic Execution and other Abstract Domains. [1]
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.

Visualization of computation steps and their results in CPAchecker
Parallel BDDs in Java (cf. Sylvan) [1]
Implementation and Evaluation of k-Shrinkability [1, 2, 3, 4]

Topics on Reliable Benchmarking and Measurements

Assigned/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

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

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]
Assigned/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.

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.