- matheja at cs.rwth-aachen.de
- Room 4206
- +49 241 80 21210
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.
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.
My research interests include
- formal verification of heap-manipulating and probabilistic programs,
- graph grammars and graph transformations, and
- static program analysis.
- 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
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).
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.
I’m currently involved in the following teaching activities:
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)
|[bibtex] [issue]||Kevin Batz, , Joost-Pieter Katoen, Christoph Matheja. Relatively Complete Verification of Probabilistic Programs, 49 Seiten, 2020. https://arxiv.org/abs/2010.14548|
|[bibtex] [issue]||Kevin Batz, Sebastian Junges, , Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. PrIC3, 2020. https://arxiv.org/abs/2004.14835|
|[bibtex] [issue]||Christoph Matheja. Automated reasoning and randomization in separation logic, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (x, 504 Seiten) : Illustrationen, Diagramme, 2020.|
|[bibtex] [issue]||Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative separation logic, Proceedings of the ACM on programming languages 3 (POPL), pages 34, ACM, 2019.|
|[bibtex] [issue]||Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the hardness of analyzing probabilistic programs, Acta informatica 56 (3), pages 255–285, Springer, 2019.|