Thesis Projects#
I always look forward to working with students on topics related to program correctness, ranging from exploring new theory to tool development.
Looking for a thesis project?#
Most of the topics I currently offer fall into one of the three general research directions described below. However, I am fairly broad-minded about research topics and would be happy to hear your ideas! You may also want to look at the list of ongoing and completed student projects for some inspiration. If you are interested in a project or would like to learn more about the concrete topics currently offered within the section, please write me an e-mail or drop by at my office whenever the door is open.
Direction 1: Formal Methods for Probabilistic Programs
Probabilistic programs are programs with the ability to sample from probability distributions. Hence, their executions have a stochastic nature, and - in contrast to arbitrary nondeterministic programs - it makes sense to study their expected (or average) behavior. Probabilistic programs appear as implementations of randomized algorithms, where sampling is exploited to ensure that expensive executions have a low probability, in cryptographic protocols, where randomness is essential for encoding secrets, as well as in statistics and artificial intelligence, where programs are becoming a popular alternative to graphical models for describing complex distributions. The behavior of probabilistic programs is often counterintuitive — a consequence of the well-known fact that humans have difficulties reasoning about stochastic processes. In combination with their various applications, the counterintuitive nature of probabilistic programs means that ensuring their correctness must be based on verification and analysis methodologies that are rigorous, tool-supported, and, ideally, automated.
Projects in this direction generally aim to develop, improve, and evaluate such techniques.
What you can expect when working in this direction:
We will build upon rigorous theoretical foundations to develop novel analysis techniques for an agreed-upon aspect of probabilistic programs. For example, we studied formal reasoning about expected runtimes and a program’s sensitivity to small input changes in past projects.
Depending on the focus, topics may involve implementing a research prototype and evaluating to what extent the proposed foundational technique (or an existing one) can be automated.
Prior knowledge about (non-probabilistic) formal methods, logic, and probability theory is beneficial but not required.
Direction 2: Rust Verification
Rust is a modern systems programming language with a focus on performance and concurrency. Its powerful type system enables the Rust compiler to give safety guarantees, such as the absence of memory access violations and race conditions, that go well beyond other programming languages (C, C++, Java, etc.). Prusti is an extension of the Rust compiler that enables developers to annotate their programs with formal specifications that are then verified at compile-time; potential specification violations are represented just like any other compiler error. A key feature of Prusti is that it leverages Rust’s type system to reduce the number of auxiliary annotations, such as loop invariants, that are required from the user to verify a specification successfully. Prusti can thus be seen as a lightweight approach to obtain stronger safety guarantees than those already provided by the Rust compiler.
What you can expect when working in this direction:
Topics in this direction may include case studies in which you apply state-of-art verifiers to real-world programs, designing novel verification techniques for currently unsupported languages features, and implementing new features in existing tools like Prusti.
Prior knowledge about Rust, program verification, and compilers is beneficial but not required.
Direction 3: Separation Logics
Separation logic is a popular formalism for Hoare-style verification of programs that manipulate resources, such as dynamically allocated memory, linked data structures, or critical sections accessible to multiple threads. Its assertion language extends first-order logic by two connectives - the separating conjunction and the magic wand - that enable writing concise specifications of how resources can be split-up and combined again. Separation logic builds upon these connectives to champion local reasoning about the resources employed by programs. That is, program parts can be verified by considering only those resources they access - a fundamental property for building scalable verification and static analysis tools. Peter O’Hearn’s CACM article gives an excellent first introduction to separation logic. At the foundation of virtually every automated approach based on separation logic lies the entailment problem: is every model of one formula also a model of another formula? For example, deductive verifiers need to solve entailments whenever they invoke the rule of consequence. While the entailment problem is undecidable in general, its central role in verification has triggered a massive interest in decidable fragments and incomplete entailment solvers.
What you can expect when working in this direction:
Topics in this direction can be both theoretical and practical. Theoretical aspects typically involve studying the decidability and complexity of the entailment problem in an agreed-upon fragment of separation logic. Practical aspects include implementing prototypical entailment solvers and comparing them to other state-of-the-art tools.
Prior knowledge about (first-order/separation) logic, sequent calculus, and program verification is beneficial but not required.
Bachelor’s Theses#
Josefine Rosalie Balch Petersen, August Weijers, Developing an Automated Learning Environment for Program Verification
Jacob Hartmann Martens, Analysing Unsafe Code Usage in Rust
Christoffer Høeg Luplau, Analysis Visualisation Framework for Probabilistic Programs, DTU, 2023.
Massimo Hansen, Restructuring and Expanding Non-Relational Databases, DTU, 2023.
Lukas Friedlos, Verifying Rust Programs Using Floating-Point Numbers and Bitwise Operations, supervised together with Vytautas Astrauskas, ETH Zürich, 2021.
Cedric Hegglin, Counterexamples for a Rust Verifier, supervised together with Aurel Bílý, ETH Zurich, 2020.
Florian Keßler, On the Decidability of Entailment Checking in Quantitative Separation Logics, supervised together with Kevin Batz, RWTH Aachen, 2020. Florian received the CS Department Award for his thesis.
Philipp Schröer, Understanding Abstraction of Probabilistic Programs, RWTH Aachen, 2019.
Daniel Cloerkes, A Cyclic Proof System for Graph Grammar Inclusion, RWTH Aachen, 2017.
Kevin Batz, Proof Rules for Expected Run-Times of Probabilistic Programs, supervised together with Benjamin Lucien Kaminski, RWTH Aachen, 2017.
Isabelle Tülleners, Graph-based Heap Abstraction for Balanced Data Structures, RWTH Aachen, 2016.
Hanna Franzen, Graph-based Symbolic Execution for Pointer Programs with Data, RWTH Aachen, 2016.
Hannah Arndt, Heap Abstraction Beyond Context-Freeness, RWTH Aachen, 2016.
Master’s Theses#
Oliver Emil Bøving, Designing a modern program verification frontend, DTU, 2023.
Jakub Eugeniusz Janaszkiewicz, Shedding the Viper Skin: A Native Back End for Automated Rust Verification, DTU, 2023.
Simon Tobias Lund, Mechanized Ghost Code and Weakest Precondition Reasoning, supervised together with Frederik Krogsdal Jacobsen and Jørgen Villadsen, DTU, 2023.
Mai-Thi Vu Do, Helena Restorff, Zenia Kjær Termøhlen, Constraint-based Probabilistic Model Checking 4 Fun, supervised together with Alberto Lluch Lafuente, DTU, 2023.
Philipp Schröer, A Deductive Verifier for Probabilistic Programs, supervised together with Kevin Batz and Benjamin Kaminski, RWTH Aachen, 2022.
Lowis Engel, Reasoning about Complexities in a Rust Verifier, supervised together with Aurel Bílý, ETH Zürich, 2021.
Marvin Jansen, Decidability and Complexity of Entailment Checking in Quantitative Separation Logic, supervised together with Kevin Batz and Ira Fesefeldt, RWTH Aachen, 2021.
Jakob Beckmann, Verifying Safe Clients of Unsafe Code and Trait Implementations in Rust, supervised together with Federico Poli, ETH Zürich, 2020.
Johnannes Schulte, Automated Detection and Completion of Confluence for Graph Grammars, RWTH Aachen, 2019.
Sally Chau, Comparing Hierachical and On-The-Fly Model Checking for Java Pointer Programs, RWTH Aachen, 2019.
Ira Fesefeldt, Proving Termination of Pointer Programs on Top of Symbolic Execution, RWTH Aachen, 2019.
Hannah Arndt, Randomized Meldable Heaps: A more Formal Proof for a less Simple Data Structure, RWTH Aachen, 2019.
Kevin Batz, IC3 for Probabilistic Systems, supervised together with Benjamin Lucien Kaminski and Sebastian Junges, RWTH Aachen, 2019.
Fabian Schneider, A Unified Algebraic Domain for Shape Analysis, RWTH Aachen, 2018. Felix Bier, From Graph Grammars to Forest Automata and Back, RWTH Aachen, 2018.