Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja,
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants,
[Technical Report]

Vytautas Astrauskas, Aurel Bílý, Jonás Fiala, Zachary Grannan, Christoph Matheja,
Peter Müller, Federico Poli, Alexander J. Summers,
The Prusti Project: Formal Verification for Rust,
*NFM 2022*.

Christoph Matheja, Jens Pagel, Florian Zuleger,
A Decision Procedure for Guarded Separation Logic,
*to appear in ACM TOCL*.

Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll,
Foundations for Entailment Checking in Quantitative
Separation Logic,
ESOP 2022.

Aurel Bílý, Christoph Matheja, Peter Müller,
Flexible Refinement Proofs in Separation Logic,
[Technical Report]

Fabian Wolff, Aurel Bílý, Christoph Matheja, Peter Müller, Alexander J. Summers,
Modular Specification and Verification of Closures in Rust,
OOPSLA, 2021.

Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja and Philipp Schröer,
Latticed k-Induction with an Application to Probabilistic Programs,
CAV, 2021.
[Technical Report]

Ira Fesefeldt, Christoph Matheja, Thomas Noll, Johannes Schulte,
Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars,
ICGT, 2021.

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja,
Relatively Complete Verification of Probabilistic Programs, POPL, 2021.

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja,
A Pre-Expectation Calculus for Probabilistic Sensitivity, POPL, 2021.

Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, Alexander J. Summers,
How Do Programmers Use Unsafe Rust?, OOPSLA, 2020.

Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer,
PrIC3: Property Directed Reachability for MDPs, CAV, 2020.
[Technical Report]

Jens Pagel, Christoph Matheja, Florian Zuleger,
Complete Entailment Checking for Separation Logic with Inductive Definitions,
CoRR, 2020.

Christoph Matheja, Automated Reasoning and Randomization in Separation Logic, Ph.D. thesis, RWTH Aachen, 2020.

Jens Katelaan, Christoph Matheja, Florian Zuleger,
Effective Entailment Checking for Separation Logic with Inductive Definitions,
TACAS, 2019.

Mihaela Sighireanu, Juan Antonio Navarro Pérez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Tomás Vojnar, Constantin Enea, Ondrej Lengál, Chong Gao, Zhilin Wu,
SL-COMP: Competition of Solvers for Separation Logic,
TACAS, 2019.

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll,
Quantitative Separation Logic,
POPL, 2019.
[Technical Report]

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll,
A Program Analysis Perspective on Expected Sampling Times,
First International Conference on Probabilistic Programming (ProbProg), Boston, 2018.

Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen,
Rule-based Conditioning of Probabilistic Data Integration,
Proceedings of the 12th International Conference on Scalable Uncertainty Management (SUM 2018), Springer, 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.

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo,
Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms,
Journal of the ACM, 2018.

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja,
On the Hardness of Analyzing Probabilistic Programs,
Acta Informatica, 2018.

Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll,
Graph-Based Shape Analysis Beyond Context-Freeness,
SEFM, 2018.
[Technical Report]

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,
ESOP, 2018.
[Technical Report]

Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger,
Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic,
ESOP, 2017.
[Technical Report]

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja,
Inferring Covariances for Probabilistic Programs,
QEST, 2016.
[Technical Report]

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja,
Reasoning about Recursive Probabilistic Programs,
LICS, 2016.
[Technical Report]

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo,
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs,
ESOP, 2016.
[Technical Report]

Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo,
Probabilistic Programs - A Natural Model for Approximate Computations,
Workshop on Approximate Computing (AC), 2015.

Christoph Matheja, Christina Jansen, Thomas Noll,
Tree-Like Grammars and Separation Logic,
APLAS, 2015.