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 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.

Teaching

I’m currently involved in the following teaching activities:

Past teaching activities:

Publications for Christoph Matheja

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.
2016
LinkChristina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic. Technical report at arXiv number 1610.07041, 2016.
DownloadBenjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Inferring Covariances for Probabilistic Programs. Proc. of the 13th International Conference on Quantitative Evaluation of SysTems (QEST 2016), Volume 9826 of LNCS, pages 191-206, Springer, 2016.
DownloadFederico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Reasoning about Recursive Probabilistic Programs. Proc. of the 31st Annual Symposium on Logic in Computer Science (LICS 2016), pages 672-681, ACM, 2016.
DOIBenjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs (EATCS Best Paper Award). Proc. of the 25th European Symposium on Programming (ESOP 2016), Volume 9632 of LNCS, pages 364 - 389, Springer, 2016.
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.
2016
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.
2015
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.