Christoph Matheja

I am a postdoctoral researcher in the Programming Methodology Group headed by Peter Müller at ETH Zürich. Previously, 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'm broadly interested in formal program verification, i.e. applying rigorous mathematical techniques to reason about software. In particular, this includes 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

Projects

  • Prusti

    I recently joined the Prusti project at ETH Zürich. Prusti is a program verifier 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

Awards

  • I was awarded the Borcher's badge in 2020 for receiving a Ph.D. degree with distinction at RWTH Aachen University.
  • 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 Lucien 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 at RWTH Aachen University.
  • 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

External Reviewer

Journals

  • ACM Transactions on Programming Languages and Systems
  • ACM Transactions on Computational Logic

Conferences

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

Event Participation

Selected Talks

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, Sebastian Junges, Benjamin Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer, PrIC3: Property Directed Reachability for MDPs, CAV, to appear.

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.

Teaching

Lectures

I have been involved in the following teaching activities:

Seminars

I have been supervising students in the following seminars:

Thesis Projects and Internships

I am currently supervising or have been supervising the following thesis projects, internships, and student assistants.
  • Florian Keßler (supervised together with Kevin Batz), On the Decidability of Entailment Checking in Quantitative Separation Logics, bachelor thesis, RWTH Aachen, ongoing.
  • 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 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 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 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 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.