Christoph Matheja

Email: matheja at cs.rwth-aachen.de
Address: Room 4206
Ahornstraße 55
D-52074 Aachen
Phone: +49 241 80 21210

I am now working as a postdoc in the Programming Methodology Group at ETH Zürich. My new website is found here or, more generally, at cmath.eu.

Before moving to Zürich, I finished my PhD at the Software Modeling and Verification Group (MOVES) headed by Professor J.-P. Katoen in January 2020.

Thesis

My PhD thesis titled “Automated Reasoning and Randomization in Separation Logic” features

a thorough introduction to weakest precondition reasoning about recursive and heap manipulating programs with separation logic,
a novel quantitative separation logic for reasoning about expected values of probabilistic pointer programs, and
automated reasoning with separation logic about temporal properties of pointer programs as well as decision procedures for reasoning about separation logic itself.

Research

My research interests include

formal verification of heap-manipulating and probabilistic programs,
graph grammars and graph transformations, and
static program analysis.

Tools

Attestor: A tool for model-checking Java pointer programs
HARRSH: A robustness checker for symbolic heap separation logic with inductive definitions based on heap automata

Supervision

Together with Benjamin Kaminski, I supervised our student research assistant Kevin Batz. Moreover, together with Christina Jansen, I supervised our student research assistant Hannah Arndt.

I am currently supervising the following thesis projects:

Sally Chau, TBA, Master’s thesis.
Justus Fesefeldt, TBA, Master’s thesis.
Philipp Schroer, Understanding Abstraction of Probabilistic Programs, Bachelor’s thesis.
Johannes Schulze, TBA, Master’s thesis.

I have been supervising the following thesis projects and internships:

Hannah Arndt, Randomized Meldable Heaps: A more formal proof of a less simple probabilistic data structure, Master’s thesis, 2019.
Kevin Batz, TBA, Master’s thesis (together with Benjamin Kaminski and Sebastian Junges), 2019.
Fabian Schneider, A Unified Algebraic Domain for Shape Analysis, Master’s thesis, 2018.
Felix Bier, From Graph Grammars to Forest Automata and Back, Master’s thesis, 2018.
Joshua Peignier (ENS Rennes), Possibility Distribution Semantics for Probabilistic Programs with Nondeterminism, internship, 2017 (together with Benjamin Kaminski).
Daniel Cloerkes, A Cyclic Proof System for Graph Grammar Inclusion, Bachelor’s thesis, 2017.
Kevin Batz, Proof Rules for Expected Run-Times of Probabilistic Programs, Bachelor’s thesis, 2017 (together with Benjamin Kaminski).
Isabelle Tülleners, Graph-based Heap Abstraction for Balanced Data Structures, Bachelor’s thesis 2016.
Hanna Franzen, Graph-based Symbolic Execution for Pointer Programs with Data, Bachelor thesis 2016.
Hannah Arndt, Heap Abstraction Beyond Context-Freeness, Bachelor thesis, 2016.
Victor Lanvin (ENS Cachan), Comparing Automated Tools for Analysing Pointer Programs, internship. 2016 (together with Christina Jansen).

Awards

Our 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.

Our 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.

Our 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.

Teaching

I’m currently involved in the following teaching activities:

Semantics and Verification of Software (SS 19)

Past teaching activities:

Static Methods for Quantitative Program Analysis (Seminar) (WS 18/19)
Static Program Analysis (SS 18)
Formal Verification Meets Machine Learning (Seminar) (SS 18)
Semantics and Verification of Software (WS 17/18)
Foundations of Probabilistic Programming (Seminar) (WS 17/18)
Compiler Construction (SS 17)
Probabilistic Programming (WS 16/17)
Static Program Analysis (WS 16/17)
Analysis and Verification of Pointer Programs (Seminar) (WS 16/17)
Compiler Construction (SS 16)
Probabilistic Programming (Seminar) (SS 16)
Theoretical Foundations of Programming Languages (Seminar) (SS 16)
Concurrency Theory (WS 15/16)
Algorithms and Data Structures (Proseminar) (WS 15/16)
Semantics and Verification of Software (SS15)
Principles of Programming Languages (Seminar) (SS15)
Turing Award Topics (Proseminar) (WS 14/15)

Publications

2020
DOI	Christoph Matheja. Automated reasoning and randomization in separation logic, 1 Online-Ressource (x, 504 Seiten) : Illustrationen, Diagramme, 2020.
DOI	Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schroer. PrIC3: Property Directed Reachability for MDPs, 2020.
DOI	Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Relatively Complete Verification of Probabilistic Programs, 49 Seiten, 2020.
2019
DOI	Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the hardness of analyzing probabilistic programs, 255-285, Springer, 2019.
DOI	Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs, 34, ACM, 2019.
2018
DOI	Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Graph-Based Shape Analysis Beyond Context-Freeness, Software engineering and formal methods : 16th International Conference, SEFM 2018, held as part of STAF 2018, Toulouse, France, June 27-29, 2018 : proceedings / Einar Broch Johnsen, Ina Schaefer (eds.), 271-286, Springer, 2018.
DOI	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, Programming Languages and Systems : 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings / edited by Amal Ahmed, 186-213, Springer, 2018.
DOI	Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic : A Logic for Reasoning about Probabilistic Programs, 159 Seiten, 2018.
DOI	Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Let this Graph Be Your Witness! : An Attestor for Verifying Java Pointer Programs, Computer Aided Verification : 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II / edited by Hana Chockler, Georg Weissenbacher, 3-11, Springer, 2018.
DOI	Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms, 30:1-30:68, 2018.
DOI	Maurice Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. Rule-Based Conditioning of Probabilistic Data, Scalable Uncertainty Management : 12th International Conference, SUM 2018, Milan, Italy, October 3-5, 2018, Proceedings / edited by Davide Ciucci, Gabriella Pasi, Barbara Vantaggi, 290-305, Springer International Publishing, 2018.
DOI	Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic, LPAR-22 : 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning / editors: Gilles Barthe, Geoff Sutcliffe and Margus Veanes, 23-36, EasyChair, 2018.
2017
DOI	Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, Programming languages and systems : 26th European Symposium on Programming, ESOP 2017, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017 : proceedings / Hongseok Yang (ed.), 611-638, Springer, 2017.
DOI	Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Heap Abstraction Beyond Context-Freeness, 44 Seiten, 2017.
2016
DOI	Federico Olmedo Beron, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Reasoning about Recursive Probabilistic Programs, Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2016) : July 5-8, 2016 New York City, USA / LICS General Chair: Martin Grohe; LICS Conference Chair: Eric Koskinen; LICS Program Chair: Natarajan Shankar, 672-681, ACM Press, 2016.
DOI	Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Inferring Covariances for Probabilistic Programs, Quantitative evaluation of systems : 13th international conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016 : proceedings / Gul Agha, Benny Van Houdt (eds.), 191-206, Springer International Publishing, 2016.
DOI	Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo Beron. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs, Programming languages and systems : 25th European Symposium on Programming, ESOP 2016, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016 : proceedings / Peter Thiemann (eds.), 364-389, Springer, 2016.
DOI	Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, 115 Seiten, 2016.
2015
DOI	Christoph Matheja, Christina Jansen, Thomas Noll. Tree-Like Grammars and Separation Logic, Programming languages and systems : 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings / edited by Xinyu Feng, Sungwoo Park, 90-108, Springer International Publishing, 2015.
	Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Probabilistic Programs - A Natural Model for Approximate Computations, [Workshop on Approximate Computing, AC15, 2015-10-15 - 2015-10-16, Paderborn, Germany], 2015.