We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
2 papers accepted at FSE 2024!

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)

Office
Room F 012, Oettingenstr. 67
E-Mail (Teaching, LMU)
firstname.lingsch@sosy.ifi.lmu.de
(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)
ORCID
0000-0002-8172-3184

Thesis Mentoring

Available topics
Crearing a deductive verifier from CPAchecker [1, 2]

Automatic software verification tries to automatically proof that a program fulfills a specification without human input. On the other hand deductive verification requires manually writing annotations to proof the program correct. Usually everything required to build a deductive verifier is inside an automatic verifier. The goal of this thesis is to create a deductive verifier out of the higly successfull automatic verifier CPAchecker.

Bridging the gap between automatic and deductive verification [1, 2]

Automatic software verification tries to automatically proof that a program fulfills a specification without human input. On the other hand deductive verification requires manually writing annotations to proof the program correct. The goal of this thesis is to combine the strengths of both approaches by writing a tools which generates proof goals using information information provided by the user, but allow some of the information to be missing for it to be automatically verified by an automatic verifier.

Witness Transfromation for: Reduction of Memory-Safety Problem of C programs to Reach-Safety Problem [1]

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. Memory-Safety and Reach-Safety property are both safety properties of the program with different atomic propositions. By instrumenting C programs, we can convert the Memory-Safety property to the Reach-Safety property, which opens new options for Memory-Safety analysis using algorithms that are used for Reach-safety tasks. After having solved the transformed task, we want to transform the witness i.e. the information the verifier provided for the verdict of the program to a witness for the original program. The goal of the thesis is to implement such a transformation of witnesses.

Reduction of No-Overflow Problem of C programs to Reach-Safety Problem [1]

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. No-Overflow and Reach-Safety property are both safety properties of the program with different atomic propositions. By instrumenting C programs, we can convert the No-Overflow property to the Reach-Safety property, which opens new options for No-Overflow analysis using algorithms that are used for Reach-safety tasks. The goal of the thesis is to develop an idea of transformation C programs so that Reach-Safety analysis proves No-Overflow, implement the transformation in a tool and observe whether it is more efficient to solve No-Overflow using Reach-Safety analysis.

Reduction of No-Datarace Problem of C programs to Reach-Safety Problem [1]

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. No-Datarace and Reach-Safety property are both safety properties of the program with different atomic propositions. By instrumenting C programs, we can convert the No-Datarace property to the Reach-Safety property, which opens new options for No-Datarace analysis using algorithms that are used for Reach-safety tasks. The goal of the thesis is to develop an idea of transformation C programs so that Reach-Safety analysis proves No-Datarace, implement the transformation in a tool and observe whether it is more efficient to solve No-Overflow using Reach-Safety analysis.

Reduction of Memory-Safety Problem of C programs to Reach-Safety Problem [1]

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. Memory-Safety and Reach-Safety property are both safety properties of the program with different atomic propositions. By instrumenting C programs, we can convert the Memory-Safety property to the Reach-Safety property, which opens new options for Memory-Safety analysis using algorithms that are used for Reach-safety tasks. The goal of the thesis is to develop an idea of transformation C programs so that Reach-Safety analysis proves Memory-Safety, implement the transformation in a tool and observe whether it is more efficient to solve Memory-Safety using Reach-Safety analysis.

Reduction of Thread-Liveness Problem of C programs to Reach-Safety Problem [1]

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. Thread-Liveness property is a liveness property, whereas Reach-Safety is a safety property. It is well-known that liveness can be transformed to safety. By instrumenting C programs, we can convert the Thread-Liveness property to the Reach-Safety property, which opens new options for Thread-Liveness analysis using algorithms that are used for Reach-safety tasks. The goal of the thesis is to implement the transformation in a tool and observe whether it is more efficient to solve Thread-Liveness using Reach-Safety analysis.

Finding Semantically Equivalent Correctness Witnesses [1, 2]

Correctness Witnesses are an artifact produced by a verifier which allows a validator to replay the verification process. The task would be to analyze correctness witnesses and find semantically equivalent witnesses from the perspective of a validator.

Modular Distributed Summary Synthesis

Due to the rising availability of distributed computational power distributing a verifier is of great interest. While distributing a single verifier is important, we consider how to use verifiers as building blocks in order to achieve distributed verification. Your goal would be to create a framework to make this possible, based upon some existing theory.

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.

Taint Analysis using CPAchecker [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 for taint analysis. The goal of this thesis would be to implement taint analysis in CPAchecker and evaluating it on a set of benchmarks.

Adding support for Hyperproperties in CPAchecker [1, 2, 3]

CPAchecker is a very successfull tool for model checking. Currently it lacks support for different Hyperproperties, for example secure information flow. Goal of this thesis would be to add support for Hyperproperties to CPAchecker.

Performance on Real-World Programs: A Case Study

Verifiers can proof different properties about many different programs. However, it is not clear how well they perform on real-world programs. The goal of this thesis would be to evaluate the performance of different verifiers on a set of real-world programs.

Inferring Predicates and Interpolants using Machine Learning [1, 2, 3]

Finding good predicates is a key challenge for verifying programs using predicate analysis. Currently some heuristics and interpolation techniques are used to find new predicates. On the other hand machine learning techniques have been succesfull in determining invariants for programs. The goal of this thesis would be to use the information generated during the exploration of the state-space of a program to find good predicates/interpolants using machine learning techniques.

Building a Deductive Verifier using an Automatic Verifier and E-ACSL [1, 2]

Deductive and Automatic Verifiers are two classes of verification methods to proof the safety of program. In this thesis the goal is to close the gap between them by transoforming an annotated program into proof goals and then using an automatic verifier to proof them. Building such a tool would be based upon a tool to treat Verifiers as SMT solvers which understand the intricacies of programming languages.

Any to Any specification transformation [1]

A verifier tries to proof that a property holds for a program. There are multiple properties a verifier can usually proof, for example Termination, Reachability, Memory Safety, etc.... Verifiers usually specialize on a couple of properties and optimize their algorithms for it. The goal of this thesis would be to implement a tool which does program transformation from any specification to any other and compare the performance of different verifiers on them.

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.

Currently assigned topics
Implementing and Evaluating a new CPA for validating and finding tubes. [1, 2]

Finding and fixing bugs is one of the most expensive parts of the software development process. To expedite it, a good description of all inputs which result in the same error can be helpful. To generate them, we will use CPAchecker to find constraints which result in an error when fulfilled, for example all even numbers as input result in an error. This will be done by first finding an error path in the program being analyzed, followed by refining a first guess for a constraint using an approach based on CEGAR.

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.