Christoph Matheja

matheja at
Room 4206
Ahornstra├če 55
D-52074 Aachen
+49 241 80 21210


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.


  • Attestor: A shape analysis tool based on graph grammars
  • HARRSH: A robustness checker for symbolic heap separation logic with inductive definitions based on heap automata 

Supervised Theses

I currently supervise or have been supervising the following theses:

  • Felix Bier, From Graph Grammars to Forest Automata and Back, master thesis, ongoing work.
  • 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.
  • 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.


I’m currently involved in the following teaching activities:

Past teaching activities:

Publications for Christoph Matheja

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. How long, O Bayesian network, will I sample thee?. Proc. of the 27th European Symposium on Programming (ESOP 2018), [to appear], Volume of LNCS, Springer, 2018.
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

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.
Christoph Matheja. Compositional Refinement of Separation Logic with Recursive Definitions, Talk at DCON, Saarbrücken, 2016.
Christoph Matheja. Tree-Like Grammars and Separation Logic, Talk at RiSE Seminar, TU Wien, Vienna, Austria, 2016.
Christoph Matheja. Tree-Like Grammars and Separation Logic, Talk at APLAS, Pohang, South Korea, 2015.
Christoph Matheja. Tree-like Grammars and Separation Logic, Talk at KPS 2015, Pörtschach, Austria, 2015.