We are hiring new student research assistants and tutors. Apply now!
Paper accepted at CCS 2023: Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications

Marian Lingsch-Rosenfeld

Picture of Marian Lingsch-Rosenfeld

Software and Computational Systems Lab
Department of Computer Science
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538 Munich (Germany)

Room F 012, Oettingenstr. 67
E-Mail (Teaching, LMU)
(Please replace "firstname" with my first name)
Office Hours
by appointment, just write me an e-mail, then we can arrange a meeting via meet.lrz.de; you also have good chances to find me at chat.ifi.lmu.de (RBG Information about the chat)

Thesis Mentoring

Available topics
Analysing the effect of compiler optimizations on Verifier performance [1, 2, 3]

It has been shown that program transformations can improve the performance of verifiers. Compilers manage to produce highly optimized code which usually contains less instructions, loops and function calls. In this thesis your job will be to analyze what compiler optimizations improve verification tasks and generate a heuristic which optimization options should be used for what programs. A rudimentary framework to run experiments already exists.

Comparing the performance increase different invariant generators have for K-Induction [1, 2, 3]

K-Induktion is an analysis which uses candidate invariants to proof the safety of a program. These candidate invariants are currently obtained from a dataflow analysis inside CPAchecker. There are a lot of tools which produce different invariants for C-Programs, it would be interesting to see if they can help improve K-Induction.

Towards CPAchecker as a static analyzer [1, 2]

CPAchecker is a very successfull tool for model checking. In particular it contains a lot of the components required to make use of it as a static analyzer, especially for slicing. The goal of this thesis would be to start the process of making CPAchecker a static analyzer by implementing a slicing CPA and evaluating it on a set of benchmarks.

Dynamic control-flow modifications for CPAchecker [1]

It has been shown that program transformations can improve the performance of verifiers. Currently most approaches to program transformations change the code without using information collected during the verification process. The goal of this thesis is to improve upon this by developing some transformations on the source code of a program which make verification easier and incorporate information collected during the verification process.

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.