Christoph Matheja

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

I am now working as a postdoc in the Programming Methodology Group at ETH Zürich. My new website is found here or, more generally, at cmath.eu.

Before moving to Zürich, I finished my PhD at the Software Modeling and Verification Group (MOVES) headed by Professor J.-P. Katoen in January 2020.

Thesis

My PhD thesis titled “Automated Reasoning and Randomization in Separation Logic” features

  1. a thorough introduction to weakest precondition reasoning about recursive and heap manipulating programs with separation logic,
  2. a novel quantitative separation logic for reasoning about expected values of probabilistic pointer programs, and
  3. automated reasoning with separation logic about temporal properties of pointer programs as well as decision procedures for reasoning about separation logic itself.

Research

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.
  • Johannes 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:

2020
DOI fulltext PDF [bibtex]
@phdthesis{A2020,
title = {Automated reasoning and randomization in separation logic},
author = {Christoph Matheja},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (x, 504 Seiten) : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-00940},
url = { https://publications.rwth-aachen.de/record/780877},
}×
[issue] 		Christoph Matheja. Automated reasoning and randomization in separation logic, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (x, 504 Seiten) : Illustrationen, Diagramme, 2020.
arXiv:2004.14835 [bibtex]
@unpublished{PPDRM2020,
title = {PrIC3: Property Directed Reachability for MDPs},
author = {Kevin Batz and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schroer},
type = {Preprint},
year = {2020},
url = { https://arxiv.org/abs/2004.14835},
}×
[issue] 		Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schroer. PrIC3: Property Directed Reachability for MDPs, 2020. https://arxiv.org/abs/2004.14835
arXiv:2010.14548 [bibtex]
@unpublished{RCVPP2020,
title = {Relatively Complete Verification of Probabilistic Programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
pages = {49 Seiten},
type = {Preprint},
year = {2020},
url = { https://arxiv.org/abs/2010.14548},
}×
[issue] 		Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Relatively Complete Verification of Probabilistic Programs, 49 Seiten, 2020. https://arxiv.org/abs/2010.14548
DOI fulltext PDF [bibtex]
@conference{PPDRM2020,
title = {PrIC3: Property Directed Reachability for MDPs},
author = {Kevin Batz and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
publisher = {Springer},
booktitle = {LNCS},
volume = {12225},
pages = {512-538},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-53291-8_27},
url = { https://publications.rwth-aachen.de/record/816242},
}×
[issue] 		Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. PrIC3: Property Directed Reachability for MDPs, 32. International Conference on Computer Aided Verification (CAV 2020), Volume 12225 of LNCS, 512-538, Springer, 2020.
fulltext PDF [bibtex]
@conference{VPP2020,
title = {Verifying Probabilistic Programs},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {12289},
pages = {298-298},
type = {Conference Paper},
year = {2020},
url = { https://publications.rwth-aachen.de/record/834060},
}×
[issue] 		Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Verifying Probabilistic Programs, 17. International Conference on Quantitative Evaluation of SysTems (QEST 2020), Volume 12289 of LNCS, 298-298, Springer, 2020.
2019
DOI [bibtex]
@article{O2019,
title = {On the hardness of analyzing probabilistic programs},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
journal = {Acta informatica},
volume = {56(3)},
pages = {pages 255-285},
type = {Journal Article},
year = {2019},
doi = {10.1007/s00236-018-0321-1},
url = { https://publications.rwth-aachen.de/record/753077},
}×
[issue] 		Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the hardness of analyzing probabilistic programs, Acta informatica 56 (3), pages 255-285, Springer, 2019.
DOI fulltext PDF [bibtex]
@article{Q2019,
title = {Quantitative separation logic: a logic for reasoning about probabilistic pointer programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {3(POPL)},
pages = {pages 34},
type = {Journal Article},
year = {2019},
doi = {10.1145/3290347},
url = { https://publications.rwth-aachen.de/record/753722},
}×
[issue] 		Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs, Proceedings of the ACM on programming languages 3 (POPL), pages 34, ACM, 2019.
2018
DOI [bibtex]
@conference{GBSABCF2018,
title = {Graph-Based Shape Analysis Beyond Context-Freeness},
author = {Hannah Arndt and Christina Jansen and Christoph Matheja and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {10886},
pages = {271-286},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-92970-5_17},
url = { https://publications.rwth-aachen.de/record/748905},
}×
[issue] 		Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Graph-Based Shape Analysis Beyond Context-Freeness, 16. International Conference on Software Engineering and Formal Methods (SEFM 2018), Volume 10886 of LNCS, 271-286, Springer, 2018.
DOI fulltext PDF [bibtex]
@conference{HOBIA2018,
title = {How long, O Bayesian network, will I sample thee?: A program analysis perspective on expected sampling times},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {10801},
pages = {186-213},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-89884-1_7},
url = { https://publications.rwth-aachen.de/record/753062},
}×
[issue] 		Kevin 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, 27. European Symposium on Programming (ESOP 2018), Volume 10801 of LNCS, 186-213, Springer, 2018.
arXiv:1802.10467 [bibtex]
@unpublished{QSLALRPP2018,
title = {Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
pages = {159 Seiten},
type = {Preprint},
year = {2018},
url = { https://arxiv.org/abs/1802.10467},
}×
[issue] 		Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Programs, 159 Seiten, 2018. https://arxiv.org/abs/1802.10467
DOI [bibtex]
@conference{LGBYWAAVJPP2018,
title = {Let this Graph Be Your Witness!: An Attestor for Verifying Java Pointer Programs},
author = {Hannah Arndt and Christina Jansen and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {10982},
pages = {3-11},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-96142-2_1},
url = { https://publications.rwth-aachen.de/record/753069},
}×
[issue] 		Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Let this Graph Be Your Witness!: An Attestor for Verifying Java Pointer Programs, 30. International Conference on Computer Aided Verification (CAV 2018), Volume 10982 of LNCS, 3-11, Springer, 2018.
DOI [bibtex]
@article{WPRERRA2018,
title = {Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Federico Olmedo},
journal = {Journal of the ACM},
volume = {65(5)},
pages = {pages 30:1-30:68},
type = {Journal Article},
year = {2018},
doi = {10.1145/3208102},
url = { https://publications.rwth-aachen.de/record/753072},
}×
[issue] 		Benjamin 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.
DOI [bibtex]
@conference{RBCPD2018,
title = {Rule-Based Conditioning of Probabilistic Data},
author = {Maurice van Keulen and Benjamin Lucien Kaminski and Christoph Matheja and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {Lecture Notes in Artificial Intelligence},
volume = {11142},
pages = {290-305},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-030-00461-3_20},
url = { https://publications.rwth-aachen.de/record/753086},
}×
[issue] 		Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. Rule-Based Conditioning of Probabilistic Data, 12. International Conference on Scalable Uncertainty Management (SUM 2018), Volume 11142 of Lecture Notes in Artificial Intelligence, 290-305, Springer, 2018.
DOI [bibtex]
@conference{HATURSHSL2018,
title = {Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic},
author = {Jens Katelaan and Christoph Matheja and Thomas Noll and Florian Zuleger},
publisher = {EasyChair},
booktitle = {EPiC series in computing},
volume = {57},
pages = {23-36},
type = {Conference Paper},
year = {2018},
doi = {10.29007/qwd8},
url = { https://publications.rwth-aachen.de/record/753090},
}×
[issue] 		Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic, 13. International Workshop on the Implementation of Logics (IWIL 2018), Volume 57 of EPiC series in computing, 23-36, EasyChair, 2018.
2017
DOI [bibtex]
@conference{URRPSHSL2017,
title = {Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic},
author = {Christina Jansen and Jens Katelaan and Christoph Matheja and Thomas Noll and Florian Zuleger},
publisher = {Springer},
booktitle = {LNCS},
volume = {10201},
pages = {611-638},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-662-54434-1_23},
url = { https://publications.rwth-aachen.de/record/713570},
}×
[issue] 		Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, 26. European Symposium on Programming (ESOP 2017), Volume 10201 of LNCS, 611-638, Springer, 2017.
arXiv:1705.03754 [bibtex]
@unpublished{HABCF2017,
title = {Heap Abstraction Beyond Context-Freeness},
author = {Hannah Arndt and Christina Jansen and Christoph Matheja and Thomas Noll},
pages = {44 Seiten},
type = {Preprint},
year = {2017},
url = { https://arxiv.org/abs/1705.03754},
}×
[issue] 		Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Heap Abstraction Beyond Context-Freeness, 44 Seiten, 2017. https://arxiv.org/abs/1705.03754
2016
DOI [bibtex]
@conference{RRPP2016,
title = {Reasoning about Recursive Probabilistic Programs},
author = {Federico Olmedo Beron and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {ACM Press},
pages = {672-681},
type = {Conference Paper},
year = {2016},
doi = {10.1145/2933575.2935317},
url = { https://publications.rwth-aachen.de/record/680115},
}×
[issue] 		Federico Olmedo Beron, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Reasoning about Recursive Probabilistic Programs, 31. Annual ACM/IEEE Symposium, 672-681, ACM Press, 2016.
DOI [bibtex]
@conference{ICPP2016,
title = {Inferring Covariances for Probabilistic Programs},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {9826},
pages = {191-206},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-43425-4_14},
url = { https://publications.rwth-aachen.de/record/680858},
}×
[issue] 		Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Inferring Covariances for Probabilistic Programs, 13. International Conference on Quantitative Evaluation of Systems (QEST 2016), Volume 9826 of LNCS, 191-206, Springer, 2016.
DOI [bibtex]
@conference{WPRERTPP2016,
title = {Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Federico Olmedo Beron},
publisher = {Springer},
booktitle = {LNCS},
volume = {9632},
pages = {364-389},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-662-49498-1_15},
url = { https://publications.rwth-aachen.de/record/684643},
}×
[issue] 		Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo Beron. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs, 25. European Symposium on Programming (ESOP 2016), Volume 9632 of LNCS, 364-389, Springer, 2016.
arXiv:1610.07041 [bibtex]
@unpublished{URRPSHSL2016,
title = {Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic},
author = {Christina Jansen and Jens Katelaan and Christoph Matheja and Thomas Noll and Florian Zuleger},
pages = {115 Seiten},
type = {Preprint},
year = {2016},
url = { https://arxiv.org/abs/1610.07041},
}×
[issue] 		Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, 115 Seiten, 2016. https://arxiv.org/abs/1610.07041
2015
DOI [bibtex]
@conference{TLGSL2015,
title = {Tree-Like Grammars and Separation Logic},
author = {Christoph Matheja and Christina Jansen and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {9458},
pages = {90-108},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-26529-2_6},
url = { https://publications.rwth-aachen.de/record/571620},
}×
[issue] 		Christoph Matheja, Christina Jansen, Thomas Noll. Tree-Like Grammars and Separation Logic, 13. Asian Symposium on Programming Languages and Systems (APLAS 2015), Volume 9458 of LNCS, 90-108, Springer, 2015.
[bibtex]
@conference{PPANMAC2015,
title = {Probabilistic Programs - A Natural Model for Approximate Computations},
author = {Nils Jansen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Federico Olmedo},
type = {Conference Paper},
year = {2015},
url = { https://publications.rwth-aachen.de/record/571634},
}×
[issue] 		Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Probabilistic Programs - A Natural Model for Approximate Computations, Workshop on Approximate Computing (AC15), 2015.