Christoph Matheja

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

Research

I am a PhD student at the Software Modeling and Verification Group (MOVES) headed by Professor J.-P. Katoen. 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.
  • Bernhard 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:

Past teaching activities:

Publications for Christoph Matheja

2019
DownloadBenjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the Hardness of Analyzing Probabilistic Programs. Acta Informatica 56(3), pages 255-285, 2019.
DOIKevin 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:1-34:29, 2019.
DOIJens Katelaan, Christoph Matheja, Florian Zuleger. Effective Entailment Checking for Separation Logic with Inductive Definitions. TACAS, Volume 11428 of LNCS, pages 319-336, Springer, 2019.
2018
DOIMaurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. Rule-based Conditioning of Probabilistic Data Integration (Best Paper Award). Proc. of the 12th International Conference on Scalable Uncertainty Management (SUM 2018), Volume 11142 of LNAI, pages 290-305, Springer, 2018.
Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. A Program Analysis Perspective on Expected Sampling Times. Collected Abstracts of the 1st International Conference on Probabilistic Programming (PROBPROG 2018), 2018.
DOIBenjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. Journal of the ACM 65(5), pages 30:1-30:68, 2018.
DownloadKevin 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.. Proc. of the 27th European Symposium on Programming (ESOP 2018), Volume 10801 of LNCS, pages 186-213, Springer, 2018.
LinkKevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic. Technical report at arxiv number 1802.10467, 2018.
DOIHannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs. Proc. CAV 2018, Part II, Volume 10982 of LNCS, pages 3–11, Springer, 2018.
DOIHannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Graph-Based Shape Analysis Beyond Context-Freeness. Proc. 16th Int. Conf. on Software Engineering and Formal Methods (SEFM 2018), Volume 10886 of LNCS, pages 271–286, Springer, 2018.
DOIJens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Harrsh: A Tool for Unified Reasoning about Symbolic-Heap Separation Logic. 13th International Workshop on the Implementation of Logics (IWIL 2018), Volume 9 of Kalpa Publications in Computing, pages 23–36, , 2018.
Show all

Selected Talks

2018
Christoph Matheja. Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs, Talk at CAV, Oxford, United Kingdom, 2018.
Christoph Matheja. Graph-Based Shape Analysis Beyond Context-Freeness, Talk at SEFM, Toulouse, France, 2018.
Show all