Christoph Matheja

61 papers A* 1A 5B 3Journal 31Unranked 16
YearRankTypeTitle / Venue / Authors
2026 J jnl
CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems (Technical Report).
CoRR
Roberto Pettinau, Christoph Matheja
2026 — conf
CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems.
TACAS (2)
Roberto Pettinau, Christoph Matheja
2025 — conf
Probabilistic Programming for Trace Generation (and Beyond).
PNSE/ATAED/PeNGE@PETRI NETS
Martin Kuhn, Joscha Grüger, Christoph Matheja, Andrey Rivkin
2024 — conf
A Game-Based Semantics for the Probabilistic Intermediate Verification Language HeyVL.
AISoLA
Christoph Matheja
2024 A conf
Data Petri Nets Meet Probabilistic Programming.
BPM
Martin Kuhn, Joscha Grüger, Christoph Matheja, Andrey Rivkin
2024 J jnl
Data Petri Nets meet Probabilistic Programming (Extended version).
CoRR
Martin Kuhn, Joscha Grüger, Christoph Matheja, Andrey Rivkin
2024 — conf
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.
Principles of Verification (1)
Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja, Tobias Winkler
2024 J jnl
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).
CoRR
Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja, Tobias Winkler
2024 — conf
LogPPL: A Tool for Probabilistic Process Mining.
ICPM Doctoral Consortium / Demo
Martin Kuhn, Joscha Grüger, Christoph Matheja, Andrey Rivkin
2024 — ed.
Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part I
Principles of Verification (1)
Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk
2024 — ed.
Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part II
Principles of Verification (2)
Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk
2024 — ed.
Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III
Principles of Verification (3)
Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk
2024 — conf
What Should Be Observed for Optimal Reward in POMDPs?
CAV (3)
Alyzia-Maria Konsta, Alberto Lluch-Lafuente, Christoph Matheja
2024 J jnl
What should be observed for optimal reward in POMDPs?
CoRR
Alyzia-Maria Konsta, Alberto Lluch-Lafuente, Christoph Matheja
2023 J jnl
A Calculus for Amortized Expected Runtimes.
Proc. ACM Program. Lang.
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht
2023 J jnl
A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions.
ACM Trans. Comput. Log.
Christoph Matheja, Jens Pagel, Florian Zuleger
2023 J jnl
A Deductive Verification Infrastructure for Probabilistic Programs.
CoRR
Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2023 J jnl
A Deductive Verification Infrastructure for Probabilistic Programs.
Proc. ACM Program. Lang.
Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2023 — conf
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants.
TACAS (2)
Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2022 J jnl
A Calculus for Amortized Expected Runtimes.
CoRR
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht
2022 J jnl
Foundations for Entailment Checking in Quantitative Separation Logic (extended version).
CoRR
Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll
2022 A conf
Foundations for Entailment Checking in Quantitative Separation Logic.
ESOP
Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll
2022 J jnl
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants.
CoRR
Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2022 — conf
The Prusti Project: Formal Verification for Rust.
NFM
Vytautas Astrauskas, Aurel Bílý, Jonás Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, Alexander J. Summers
2021 J jnl
A pre-expectation calculus for probabilistic sensitivity.
Proc. ACM Program. Lang.
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2021 B conf
Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars.
ICGT
Ira Fesefeldt, Christoph Matheja, Thomas Noll, Johannes Schulte
2021 J jnl
Flexible Refinement Proofs in Separation Logic.
CoRR
Aurel Bílý, Christoph Matheja, Peter Müller
2021 — conf
Latticed k-Induction with an Application to Probabilistic Programs.
CAV (2)
Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
2021 J jnl
Latticed k-Induction with an Application to Probabilistic Programs.
CoRR
Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
2021 J jnl
Modular specification and verification of closures in Rust.
Proc. ACM Program. Lang.
Fabian Wolff, Aurel Bílý, Christoph Matheja, Peter Müller, Alexander J. Summers
2021 J jnl
Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning.
Proc. ACM Program. Lang.
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2020 — —
Automated reasoning and randomization in separation logic.
Christoph Matheja
2020 J jnl
Complete Entailment Checking for Separation Logic with Inductive Definitions.
CoRR
Jens Pagel, Christoph Matheja, Florian Zuleger
2020 — ch.
Expected Runtime Analyis by Program Verification.
Foundations of Probabilistic Programming
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2020 J jnl
How do programmers use unsafe rust?
Proc. ACM Program. Lang.
Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, Alexander J. Summers
2020 — conf
PrIC3: Property Directed Reachability for MDPs.
CAV (2)
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
2020 J jnl
PrIC3: Property Directed Reachability for MDPs.
CoRR
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
2020 J jnl
Relatively Complete Verification of Probabilistic Programs.
CoRR
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2019 — conf
Effective Entailment Checking for Separation Logic with Inductive Definitions.
TACAS (2)
Jens Katelaan, Christoph Matheja, Florian Zuleger
2019 J jnl
Kantorovich Continuity of Probabilistic Programs.
CoRR
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2019 J jnl
On the hardness of analyzing probabilistic programs.
Acta Informatica
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2019 J jnl
Quantitative separation logic: a logic for reasoning about probabilistic pointer programs.
Proc. ACM Program. Lang.
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll
2019 — conf
SL-COMP: Competition of Solvers for Separation Logic.
TACAS (3)
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
2018 B conf
Graph-Based Shape Analysis Beyond Context-Freeness.
SEFM
Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll
2018 — conf
Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic.
LPAR (Workshop and Short Papers)
Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger
2018 A conf
How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times.
ESOP
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2018 J jnl
How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times.
CoRR
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2018 — conf
Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs.
CAV (2)
Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll
2018 J jnl
Quantitative Separation Logic.
CoRR
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll
2018 — conf
Rule-Based Conditioning of Probabilistic Data.
SUM
Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen
2018 J jnl
Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms.
J. ACM
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo
2017 J jnl
Heap Abstraction Beyond Context-Freeness.
CoRR
Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll
2017 A conf
Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic.
ESOP
Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger
2016 — conf
Inferring Covariances for Probabilistic Programs.
QEST
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2016 J jnl
Inferring Covariances for Probabilistic Programs.
CoRR
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2016 A* conf
Reasoning about Recursive Probabilistic Programs.
LICS
Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2016 J jnl
Reasoning about Recursive Probabilistic Programs.
CoRR
Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2016 J jnl
Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic.
CoRR
Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger
2016 A conf
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs.
ESOP
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo
2016 J jnl
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs.
CoRR
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo
2015 B conf
Tree-Like Grammars and Separation Logic.
APLAS
Christoph Matheja, Christina Jansen, Thomas Noll