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.

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

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

I currently supervise or have been supervising the following thesis projects and internships:

  • Fabian Schneider, A Unified Algebraic Domain for Shape Analysis, master thesis, 2018.
  • Felix Bier, From Graph Grammars to Forest Automata and Back, master 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 thesis, 2017.
  • Kevin Batz, Proof Rules for Expected Run-Times of Probabilistic Programs, bachelor thesis, 2017 (together with Benjamin Kaminski).
  • Isabelle Tülleners, Graph-based Heap Abstraction for Balanced Data Structures, bachelor 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 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

2018
Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. Rule-based Conditioning of Probabilistic Data Integration. Proc. of the 12th International Conference on Scalable Uncertainty Management (SUM 2018), Volume of LNAI, 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.
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.
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. Journal of the ACM [to appear], 2018.
DownloadBenjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the Hardness of Analyzing Probabilistic Programs. Acta Informatica [to appear], 2018.
2017
LinkHannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Heap Abstraction Beyond Context-Freeness. Technical report at arxiv number 1705.03754, 2017.
DOIChristina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic. Proc. ESOP 2017, Volume 10201 of LNCS, pages 611–638, Springer, 2017.
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.
2017
Christoph Matheja. Heap Automata, Talk at NII Shonan Meeting, Hayama Miura-gun, Japan, 2017.
Christoph Matheja. A Program Analysis Perspective on Expected Sampling Times, Talk at ROCKS, Münster, Germany, 2017.
Christoph Matheja. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, Talk at ESOP, Uppsala, Sweden, 2017.
Show all