Christoph Matheja

I'm a researcher with interest in reasoning about program correctness in a broad sense. I'm always looking for motivated students and interns to work with on a variety of topics (see below for details).

In November 2021, I joined the formal methods section of the Technical University of Denmark (DTU) as an assistant professor. Previously, I was as a postdoctoral researcher in the Programming Methodology Group headed by Peter Müller at ETH Zürich. Before that, I was a Ph.D. student in the Software Modeling and Verification Group at RWTH Aachen University under the supervision of Joost-Pieter Katoen. I defended my Ph.D. thesis titled "Automated Reasoning and Randomization in Separation Logic" [pdf] in January 2020.

Research Interests

I work in the general area of formal methods and program verifcation, that is, applying rigorous mathematical techniques to reason about software. In particular, my previous research includes techniques for formal reasoning about heap-manipulating and probabilistic programs. To this end, I have worked with Hoare-style and weakest-precondition-style proof systems, separation logic, graph grammars, model-checking, and abstract interpretation.

Christoph Matheja

Contact

Email
chmat (at) dtu (dot) dk
Address
DTU Lyngby Campus, building 321, room 009
Platforms

Projects

  • Prusti

    Prusti is a program verifier developed at ETH Zurich for the Rust programming language that is build on top of Viper. It exploits Rust's type system to automatically derive a core proof for, amongst others, memory safety. This reduces the overall verification effort for functional correctness, because basic properties do not have to be specified and proved manually.

    Learn More

  • Verification of Probabilistic Programs

    Probabilistic programs are programs with the ability to flip coins. They occur, for instance, in cryptography, randomized algorithms, and as modeling language for machine learning. Instead of computing an output state for every input state, a probabilistic program thus computes a distribution of over output states. How can we formally reason about such programs?

    Learn More

  • Attestor

    Attestor is an open-source tool for model-checking Java programs operating on dynamic data structures. Its theoretical foundations are based on abstract interpretation and context-free graph grammars to describe underlying data structures. The analysis is fully automated, procedure-modular, and provides visual feedback to understand property violations.

    Attestor on GitHub

  • Decision Procedures for Separation Logic

    Separation logic is an extension of Hoare logic to write elegant rigorous proofs for heap manipulating programs. I considered techniques that enable formal reasoning about satisfiability, entailment, and other robustness properties of separation logic. These techniques have been implemented at TU Wien in an open-source tool called HARRSH.

    HARRSH on GitHub

Student Projects (bachelor's thesis, master's thesis, internships)

I always look forward to working with students on topics related to program correctness, ranging from exploring new theory to tool development—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 (chmat (at) dtu (dot) dk) or drop by at my office (Lyngby campus, building 321, room 009) whenever the door is open.

Direction A: 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.
  • Many topics consider deductive verification techniques, but we also offer topics touching model checking and static analysis.
  • Prior knowledge about (non-probabilistic) formal methods, logic, and probability theory is beneficial but not required.

Direction B: Verification of Rust Programs

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 C: Decision Procedures for Separation Logic

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.

Completed Student Projects

  • Philipp Schröer (supervised together with Kevin Batz and Benjamin Kaminski), master thesis.
  • Lowis Engel (supervised together with Aurel Bílý), Reasoning about Complexities in a Rust Verifier, master thesis, ETH Zurich, 2021.
  • Lukas Friedlos (supervised together with Vytautas Astrauskas), Verifying Rust Programs Using Floating-Point Numbers and Bitwise Operations, bachelor thesis, ETH Zurich, 2021.
  • Marvin Jansen (supervised together with Kevin Batz and Ira Fesefeldt), Decidability and Complexity of Entailment Checking in Quantitative Separation Logic, master thesis, RWTH Aachen, 2021.
  • Cedric Hegglin (supervised together with Aurel Bílý), Counterexamples for a Rust Verifier, bachelor thesis, ETH Zurich, 2020.
  • Jakob Beckmann (supervised together with Federico Poli), Verifying Safe Clients of Unsafe Code and Trait Implementations in Rust, master thesis, ETH Zurich, 2020.
  • Florian Keßler (supervised together with Kevin Batz), On the Decidability of Entailment Checking in Quantitative Separation Logics, bachelor thesis, RWTH Aachen, 2020. Florian received the CS Department Award for his thesis.
  • Johnannes Schulte, Automated Detection and Completion of Confluence for Graph Grammars, master thesis, RWTH Aachen, 2019.
  • Sally Chau, Comparing Hierachical and On-The-Fly Model Checking for Java Pointer Programs, master thesis, RWTH Aachen, 2019.
  • Ira Fesefeldt, Proving Termination of Pointer Programs on Top of Symbolic Execution, master thesis, RWTH Aachen, 2019.
  • Hannah Arndt, Randomized Meldable Heaps: A more Formal Proof for a less Simple Data Structure, master thesis, RWTH Aachen, 2019.
  • Kevin Batz (supervised together with Benjamin Lucien Kaminski and Sebastian Junges), IC3 for Probabilistic Systems, master thesis, RWTH Aachen, 2019.
  • Philipp Schröer, Understanding Abstraction of Probabilistic Programs, bachelor thesis, RWTH Aachen, 2019.
  • From 2017 to 2019, Benjamin Lucien Kaminski and I supervised Kevin Batz who worked as a student assistant on formal reasoning about expected runtimes of probabilistic programs.
  • From 2016 to 2019, I supervised Hannah Arndt who worked as a student assistant on the Attestor project..
  • Fabian Schneider, A Unified Algebraic Domain for Shape Analysis, master thesis, RWTH Aachen, 2018.
  • Felix Bier, From Graph Grammars to Forest Automata and Back, master thesis, RWTH Aachen, 2018.
  • Joshua Peignier (ENS Rennes, supervised together with Benjamin Lucien Kaminski), Possibility Distribution Semantics for Probabilistic Programs with Nondeterminism, internship, RWTH Aachen, 2017.
  • Daniel Cloerkes, A Cyclic Proof System for Graph Grammar Inclusion, bachelor thesis, RWTH Aachen, 2017.
  • Kevin Batz (supervised together with Benjamin Lucien Kaminski), Proof Rules for Expected Run-Times of Probabilistic Programs, bachelor thesis, RWTH Aachen, 2017.
  • Isabelle Tülleners, Graph-based Heap Abstraction for Balanced Data Structures, bachelor thesis, RWTH Aachen, 2016.
  • Hanna Franzen, Graph-based Symbolic Execution for Pointer Programs with Data, bachelor thesis, RWTH Aachen, 2016.
  • Hannah Arndt, Heap Abstraction Beyond Context-Freeness, bachelor thesis, RWTH Aachen, 2016.
  • Victor Lanvin (ENS Cachan, supervised together with Christina Jansen), Comparing Automated Tools for Analysing Pointer Programs, internship, RWTH Aachen, 2016.

Teaching

Lectures

Teaching Assistant

I have been involved as a teaching assistant in the following lectures:

Seminars

I have been supervising students in the following seminars:

Awards

  • The paper A Pre-Expectation Calculus for Probabilistic Sensitivity (joint work with Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Kaminski, and Joost-Pieter Katoen) has been selected as a distinguished paper at POPL 2021.
  • I was awarded the Borchers Plakette in 2020 for finishing my PhD with distinction.
  • The paper How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times (joint work with Kevin Batz, Benjamin Kaminski, and Joost-Pieter Katoen) was nominated for the EATCS Best Paper Award at ETAPS 2018.
  • The paper Rule-based Conditioning of Probabilistic Data Integration (joint work with Maurice van Keulen, Benjamin Kaminski, and Joost-Pieter Katoen) won the best paper award at SUM 2018.
  • The paper Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs (joint work with Benjamin Kaminski, Joost-Pieter Katoen, and Federico Olmedo) won the EATCS Best Paper Award for the best theory paper presented at ETAPS 2016.
  • I was awarded the Springorum Medal in 2015 for receiving a master’s degree with distinction.
  • From 2011-2013 I was put on the Dean's List at RWTH Aachen University for belonging to the top five percent of the best students in each year.

Professional Activities

Event Organization / Chair

Program Committee

Grants

  • Automated Verification of Sensitivity Properties for Probabilistic Programs, DIREC Explore Project

External Reviewer

Journals

  • ACM Transactions on Programming Languages and Systems
  • ACM Transactions on Computational Logic
  • Information Processing Letters
  • Science of Computer Programming

Conferences

POPL, OOPSLA, CONCUR, CSL, DLT, DSN, FM, FTSCS, ICALP, LATA, LICS, LPAR

Event Participation

Selected Talks

Towards Automated Verification of Probabilistic Programs, invited talk at IT University of Copenhagen, Denmark, 2022.

Towards Automated Verification of Probabilistic Programs, invited talk at Logic and Semantics Group, Aarhus University, Denmark, 2021.

Reasoning about Probabilistic Programs: From Quantitative Logics To Automated Verification, invited talk at formal methods seminar, DTU, Denmark, 2021. [slides]

Rust & Prusti: From a Safety-Focused Design To Formal Verification, invited talk organized by VIS, ETH Zurich, Switzerland, 2020. [slides]

Verifying Probabilistic Programs, Tutorial at QEST 2020.

Automated Reasoning and Randomization in Separation Logic, Ph.D. defense, RWTH Aachen, Aachen, Germany, 2020. [slides]

Quantitative Separation Logic (invited talk), ETH Zürich, Zürich, Switzerland, 2019. [slides]

Weakest Preexpectations and Quantitative Separation Logic (tutorial), DCON, Munich, Germany, 2019. [slides]

Quantitative Separation Logic (invited talk), Lorentz Center Seminar "Effective Verification: Static Analysis Meets Program Logics", Leiden, Netherlands, 2019. [slides]

Quantitative Separation Logic, POPL, Cascais, Portugal, 2019. [slides]

Quantitative Separation Logic, ROCKS Meeting, Freising, Germany, 2018. [slides]

Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs, CAV (as part of FLOC), Oxford, United Kingdom, 2018. [slides]

Graph-Based Shape Analysis Beyond Context-Freeness, SEFM, Toulouse, France, 2018. [slides]

Heap Automata (invited talk), NII Shonan Meeting on Verification of Pointer Programs, Kanagawa, Japan, 2017. [slides]

A Program Analysis Perspective on Expected Sampling Times, ROCKS Meeting, Münster, Germany, 2017. [slides]

Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, ESOP, Uppsala, Sweden, 2017. [slides]

Compositional Refinement of Separation Logic with Recursive Definitions, DCON, Saarbrücken, Germany, 2016. [slides]

Tree-Like Grammars and Separation Logic (invited talk), RiSE Seminar, TU Wien, Vienna, Austria, 2016. [slides]

Tree-Like Grammars and Separation Logic, APLAS, Pohang, South Korea, 2015. [slides]

Publications

Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants, [Technical Report]

Vytautas Astrauskas, Aurel Bílý, Jonás Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, Alexander J. Summers, The Prusti Project: Formal Verification for Rust, NFM 2022.

Christoph Matheja, Jens Pagel, Florian Zuleger, A Decision Procedure for Guarded Separation Logic, to appear in ACM TOCL.

Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll, Foundations for Entailment Checking in Quantitative Separation Logic, ESOP 2022.

Aurel Bílý, Christoph Matheja, Peter Müller, Flexible Refinement Proofs in Separation Logic, [Technical Report]

Fabian Wolff, Aurel Bílý, Christoph Matheja, Peter Müller, Alexander J. Summers, Modular Specification and Verification of Closures in Rust, OOPSLA, 2021.

Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja and Philipp Schröer, Latticed k-Induction with an Application to Probabilistic Programs, CAV, 2021. [Technical Report]

Ira Fesefeldt, Christoph Matheja, Thomas Noll, Johannes Schulte, Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars, ICGT, 2021.

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Relatively Complete Verification of Probabilistic Programs, POPL, 2021.

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, A Pre-Expectation Calculus for Probabilistic Sensitivity, POPL, 2021.

Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, Alexander J. Summers, How Do Programmers Use Unsafe Rust?, OOPSLA, 2020.

Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer, PrIC3: Property Directed Reachability for MDPs, CAV, 2020. [Technical Report]

Jens Pagel, Christoph Matheja, Florian Zuleger, Complete Entailment Checking for Separation Logic with Inductive Definitions, CoRR, 2020.

Christoph Matheja, Automated Reasoning and Randomization in Separation Logic, Ph.D. thesis, RWTH Aachen, 2020.

Jens Katelaan, Christoph Matheja, Florian Zuleger, Effective Entailment Checking for Separation Logic with Inductive Definitions, TACAS, 2019.

Mihaela Sighireanu, Juan Antonio Navarro Pérez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Tomás Vojnar, Constantin Enea, Ondrej Lengál, Chong Gao, Zhilin Wu, SL-COMP: Competition of Solvers for Separation Logic, TACAS, 2019.

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll, Quantitative Separation Logic, POPL, 2019. [Technical Report]

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll, A Program Analysis Perspective on Expected Sampling Times, First International Conference on Probabilistic Programming (ProbProg), Boston, 2018.

Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen, Rule-based Conditioning of Probabilistic Data Integration, Proceedings of the 12th International Conference on Scalable Uncertainty Management (SUM 2018), Springer, 2018.

Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll, Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs, CAV, 2018.

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo, Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms, Journal of the ACM, 2018.

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, On the Hardness of Analyzing Probabilistic Programs, Acta Informatica, 2018.

Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll, Graph-Based Shape Analysis Beyond Context-Freeness, SEFM, 2018. [Technical Report]

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times, ESOP, 2018. [Technical Report]

Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, ESOP, 2017. [Technical Report]

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Inferring Covariances for Probabilistic Programs, QEST, 2016. [Technical Report]

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Reasoning about Recursive Probabilistic Programs, LICS, 2016. [Technical Report]

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo, Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs, ESOP, 2016. [Technical Report]

Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo, Probabilistic Programs - A Natural Model for Approximate Computations, Workshop on Approximate Computing (AC), 2015.

Christoph Matheja, Christina Jansen, Thomas Noll, Tree-Like Grammars and Separation Logic, APLAS, 2015.

© Christoph Matheja, 2020. Design based on HTML5 UP.