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, ongoing work.
  • Raoul Schaffranek, Learning Heap Automata from Systems of Inductive Definitions, working title, ongoing work
  • Felix Bier, From Graph Grammars to Forest Automata and Back, master thesis, ongoing work.
  • 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
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.
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, Volume of LNCS, Springer, 2018.
Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Graph-Based Shape Analysis Beyond Context-Freeness. Proc. of the 16th International Conference on Software Engineering and Formal Methods (SEFM 2018) [to appear], Volume of LNCS, 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, pages 69, 2018.
Benjamin 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

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