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

Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. - Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Federico Olmedo (ESOP, 2016)

Reasoning about Recursive Probabilistic Programs. - Federico Olmedo; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (LICS, 2016)

Inferring Covariances for Probabilistic Programs. - Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (QEST, 2016)

Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic. - Christina Jansen; Jens Katelaan; Christoph Matheja; Thomas Noll 001; Florian Zuleger (ESOP, 2017)

Heap Abstraction Beyond Context-Freeness. - Hannah Arndt; Christina Jansen; Christoph Matheja; Thomas Noll 001 (CoRR, 2017)

Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs. - Hannah Arndt; Christina Jansen; Joost-Pieter Katoen; Christoph Matheja; Thomas Noll 001 (CAV (2), 2018)

How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times. - Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (ESOP, 2018)

Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic. - Jens Katelaan; Christoph Matheja; Thomas Noll 001; Florian Zuleger (LPAR (Workshop and Short Papers), 2018)

Graph-Based Shape Analysis Beyond Context-Freeness. - Hannah Arndt; Christina Jansen; Christoph Matheja; Thomas Noll 001 (SEFM, 2018)

Rule-Based Conditioning of Probabilistic Data. - Maurice van Keulen; Benjamin Lucien Kaminski; Christoph Matheja; Joost-Pieter Katoen (SUM, 2018)

Quantitative Separation Logic. - Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Thomas Noll 001 (CoRR, 2018)

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

Effective Entailment Checking for Separation Logic with Inductive Definitions. - Jens Katelaan; Christoph Matheja; Florian Zuleger (TACAS (2), 2019)

SL-COMP: Competition of Solvers for Separation Logic. - Mihaela Sighireanu; Juan Antonio Navarro Pérez; Andrey Rybalchenko; Nikos Gorogiannis; Radu Iosif; Andrew Reynolds 001; Cristina Serban; Jens Katelaan; Christoph Matheja; Thomas Noll 001; Florian Zuleger; Wei-Ngan Chin; et al. (TACAS (3), 2019)

On the hardness of analyzing probabilistic programs. - Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Acta Informatica, 2019)

Kantorovich Continuity of Probabilistic Programs. - Alejandro Aguirre 001; Gilles Barthe; Justin Hsu; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (CoRR, 2019)

Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. - Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Thomas Noll 001 (Proc. ACM Program. Lang., 2019)

Expected Runtime Analyis by Program Verification. - Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Foundations of Probabilistic Programming, 2020)

PrIC3: Property Directed Reachability for MDPs. - Kevin Batz; Sebastian Junges; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Philipp Schröer (CAV (2), 2020)

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

Relatively Complete Verification of Probabilistic Programs. - Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (CoRR, 2020)

How do programmers use unsafe rust? - Vytautas Astrauskas; Christoph Matheja; Federico Poli 001; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2020)

Automated reasoning and randomization in separation logic. - Christoph Matheja (2020)

Latticed k-Induction with an Application to Probabilistic Programs. - Kevin Batz; Mingshuai Chen; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Philipp Schröer (CAV (2), 2021)

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

Flexible Refinement Proofs in Separation Logic. - Aurel Bílý; Christoph Matheja; Peter Müller 001 (CoRR, 2021)

A pre-expectation calculus for probabilistic sensitivity. - Alejandro Aguirre 001; Gilles Barthe; Justin Hsu; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Proc. ACM Program. Lang., 2021)

Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. - Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Proc. ACM Program. Lang., 2021)

Modular specification and verification of closures in Rust. - Fabian Wolff; Aurel Bílý; Christoph Matheja; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2021)

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

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

Foundations for Entailment Checking in Quantitative Separation Logic (extended version). - Kevin Batz; Ira Fesefeldt; Marvin Jansen; Joost-Pieter Katoen; Florian Keßler; Christoph Matheja; Thomas Noll 001 (CoRR, 2022)

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants. - Kevin Batz; Mingshuai Chen; Sebastian Junges; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (TACAS (2), 2023)

A Calculus for Amortized Expected Runtimes. - Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Lena Verscht (Proc. ACM Program. Lang., 2023)

A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions. - Christoph Matheja; Jens Pagel; Florian Zuleger (ACM Trans. Comput. Log., 2023)

A Deductive Verification Infrastructure for Probabilistic Programs - Artifact Evaluation. - Philipp Schröer; Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Zenodo, 2023)

A Deductive Verification Infrastructure for Probabilistic Programs. - Philipp Schröer; Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Proc. ACM Program. Lang., 2023)

J-P: MDP. FP. PP - Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs. - Kevin Batz; Benjamin Lucien Kaminski; Christoph Matheja; Tobias Winkler 001 (Principles of Verification (1), 2024)

Data Petri Nets Meet Probabilistic Programming. - Martin Kuhn; Joscha Grüger; Christoph Matheja; Andrey Rivkin (BPM, 2024)

What Should Be Observed for Optimal Reward in POMDPs? - Alyzia-Maria Konsta; Alberto Lluch-Lafuente; Christoph Matheja (CAV (3), 2024)

LogPPL: A Tool for Probabilistic Process Mining. - Martin Kuhn; Joscha Grüger; Christoph Matheja; Andrey Rivkin (ICPM Doctoral Consortium / Demo, 2024)

A Game-Based Semantics for the Probabilistic Intermediate Verification Language HeyVL. - Christoph Matheja (AISoLA, 2024)

Data Petri Nets meet Probabilistic Programming (Extended version). - Martin Kuhn; Joscha Grüger; Christoph Matheja; Andrey Rivkin (CoRR, 2024)

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report). - Kevin Batz; Benjamin Lucien Kaminski; Christoph Matheja; Tobias Winkler 001 (CoRR, 2024)