R. Pettinau and C. Matheja, "CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems (Technical Report)" CoRR, vol. abs/2601.15756. 2026.
doi: 10.48550/ARXIV.2601.15756

R. Pettinau and C. Matheja, "CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems" in Proc. Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part II, 2026.
doi: 10.1007/978-3-032-22749-2_15

C. Imenkamp, J. Grüger, M. Kuhn, C. Matheja, A. Rivkin, and A. Koschmider, "YAPNE: A Tool for Modeling and Automated Verification of Data Petri Nets" in Proc. Doctoral Consortium and Demo Track 2025 at the International Conference on Process Mining 2025 co-located with the 7th International Conference on Process Mining (ICPM 2025), Montevideo, Uruguay, October 21, 2025, 2025.

M. Kuhn, J. Grüger, C. Matheja, and A. Rivkin, "Probabilistic Programming for Trace Generation (and Beyond)" in Proc. Joint Proceedings of the Workshops at the 46th International Conference on Application and Theory of Petri Nets and Concurrency: Petri Nets and Software Engineering (PNSE'25), Algorithms & Theories for the Analysis of Event Data (ATAED'25), and Petri Net Games, Examples and Quizzes for Education, Contest and Fun (PeNGE'25) co-located with PETRI NETS 2025, June 23 - 24, 2025, Paris, France, 2025.

M. Kuhn, J. Grüger, C. Matheja, and A. Rivkin, "LogPPL: A Tool for Probabilistic Process Mining" in Proc. Doctoral Consortium and Demo Track 2024 at the International Conference on Process Mining 2024 co-located with the 6th International Conference on Process Mining (ICPM 2024), Copenhagen, Denmark, October 15, 2024, 2024.

A. -, A. L. -, and C. Matheja, "What should be observed for optimal reward in POMDPs?" CoRR, vol. abs/2405.10768. 2024.
doi: 10.48550/ARXIV.2405.10768

M. Kuhn, J. Grüger, C. Matheja, and A. Rivkin, "Data Petri Nets meet Probabilistic Programming (Extended version)" CoRR, vol. abs/2406.11883. 2024.
doi: 10.48550/ARXIV.2406.11883

K. Batz, B. L. Kaminski, C. Matheja, and T. Winkler, "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, vol. abs/2411.16564. 2024.
doi: 10.48550/ARXIV.2411.16564

Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part ISpringer.
doi: 10.1007/978-3-031-75783-9

Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part IISpringer.
doi: 10.1007/978-3-031-75775-4

Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part IIISpringer.
doi: 10.1007/978-3-031-75778-5

K. Batz, B. L. Kaminski, C. Matheja, and T. Winkler, "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" in Proc. Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part I, 2024.
doi: 10.1007/978-3-031-75783-9_11

M. Kuhn, J. Grüger, C. Matheja, and A. Rivkin, "Data Petri Nets Meet Probabilistic Programming" in Proc. Business Process Management - 22nd International Conference, BPM 2024, Krakow, Poland, September 1-6, 2024, Proceedings, 2024.
doi: 10.1007/978-3-031-70396-6_2

A. -, A. L. -, and C. Matheja, "What Should Be Observed for Optimal Reward in POMDPs?" in Proc. Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III, 2024.
doi: 10.1007/978-3-031-65633-0_17

C. Matheja, "A Game-Based Semantics for the Probabilistic Intermediate Verification Language HeyVL" in Proc. Bridging the Gap Between AI and Reality - Second International Conference, AISoLA 2024, Crete, Greece, October 30 - November 3, 2024, Proceedings, 2024.
doi: 10.1007/978-3-031-75434-0_17

P. Schröer, K. Batz, B. L. Kaminski, J. -, and C. Matheja, "A Deductive Verification Infrastructure for Probabilistic Programs" CoRR, vol. abs/2309.07781. 2023.
doi: 10.48550/ARXIV.2309.07781

K. Batz, B. L. Kaminski, J. -, C. Matheja, and L. Verscht, "A Calculus for Amortized Expected Runtimes" Proc. ACM Program. Lang. vol. 7, iss. POPL. 2023.
doi: 10.1145/3571260

P. Schröer, K. Batz, B. L. Kaminski, J. -, and C. Matheja, "A Deductive Verification Infrastructure for Probabilistic Programs" Proc. ACM Program. Lang. vol. 7, iss. OOPSLA2. 2023.
doi: 10.1145/3622870

C. Matheja, J. Pagel, and F. Zuleger, "A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions" ACM Trans. Comput. Log. vol. 24, iss. 1. 2023.
doi: 10.1145/3534927

P. Schröer, K. Batz, B. L. Kaminski, J. -, and C. Matheja. () A Deductive Verification Infrastructure for Probabilistic Programs - Artifact Evaluation (Version 1). [Online]. Available: https://doi.org/10.5281/zenodo.8146987
doi: 10.5281/ZENODO.8146987

K. Batz, M. Chen, S. Junges, B. L. Kaminski, J. -, and C. Matheja, "Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants" in Proc. Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, 2023.
doi: 10.1007/978-3-031-30820-8_25

K. Batz, I. Fesefeldt, M. Jansen, J. -, F. Keßler, C. Matheja, and T. Noll, "Foundations for Entailment Checking in Quantitative Separation Logic (extended version)" CoRR, vol. abs/2201.11464. 2022.

K. Batz, M. Chen, S. Junges, B. L. Kaminski, J. -, and C. Matheja, "Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants" CoRR, vol. abs/2205.06152. 2022.
doi: 10.48550/ARXIV.2205.06152

K. Batz, B. L. Kaminski, J. -, C. Matheja, and L. Verscht, "A Calculus for Amortized Expected Runtimes" CoRR, vol. abs/2211.12923. 2022.
doi: 10.48550/ARXIV.2211.12923

K. Batz, I. Fesefeldt, M. Jansen, J. -, F. Keßler, C. Matheja, and T. Noll, "Foundations for Entailment Checking in Quantitative Separation Logic" in Proc. Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, 2022.
doi: 10.1007/978-3-030-99336-8_3

V. Astrauskas, A. B\'. i, J. Fiala, Z. Grannan, C. Matheja, P. Müller, F. Poli, and A. J. Summers, "The Prusti Project: Formal Verification for Rust" in Proc. NASA Formal Methods - 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings, 2022.
doi: 10.1007/978-3-031-06773-0_5

K. Batz, M. Chen, B. L. Kaminski, J. -, C. Matheja, and P. Schröer, "Latticed k-Induction with an Application to Probabilistic Programs" CoRR, vol. abs/2105.14100. 2021.

A. B\'. i, C. Matheja, and P. Müller, "Flexible Refinement Proofs in Separation Logic" CoRR, vol. abs/2110.13559. 2021.

A. Aguirre, G. Barthe, J. Hsu, B. L. Kaminski, J. -, and C. Matheja, "A pre-expectation calculus for probabilistic sensitivity" Proc. ACM Program. Lang. vol. 5, iss. POPL. 2021.
doi: 10.1145/3434333

K. Batz, B. L. Kaminski, J. -, and C. Matheja, "Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning" Proc. ACM Program. Lang. vol. 5, iss. POPL. 2021.
doi: 10.1145/3434320

F. Wolff, A. B\'. i, C. Matheja, P. Müller, and A. J. Summers, "Modular specification and verification of closures in Rust" Proc. ACM Program. Lang. vol. 5, iss. OOPSLA. 2021.
doi: 10.1145/3485522

F. Wolff, A. B\'. i, C. Matheja, P. Müller, and A. J. Summers. () Modular Specification and Verification of Closures in Rust (artefact) (Version 1). [Online]. Available: https://doi.org/10.5281/zenodo.5482557
doi: 10.5281/ZENODO.5482557

K. Batz, M. Chen, B. L. Kaminski, J. -, C. Matheja, and P. Schröer, "Latticed k-Induction with an Application to Probabilistic Programs" in Proc. Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, 2021.
doi: 10.1007/978-3-030-81688-9_25

I. Fesefeldt, C. Matheja, T. Noll, and J. Schulte, "Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars" in Proc. Graph Transformation - 14th International Conference, ICGT 2021, Held as Part of STAF 2021, Virtual Event, June 24-25, 2021, Proceedings, 2021.
doi: 10.1007/978-3-030-78946-6_15

C. Matheja, "Automated reasoning and randomization in separation logic" PhD Thesis , 2020.

J. Pagel, C. Matheja, and F. Zuleger, "Complete Entailment Checking for Separation Logic with Inductive Definitions" CoRR, vol. abs/2002.01202. 2020.

K. Batz, S. Junges, B. L. Kaminski, J. -, C. Matheja, and P. Schröer, "PrIC3: Property Directed Reachability for MDPs" CoRR, vol. abs/2004.14835. 2020.

K. Batz, B. L. Kaminski, J. -, and C. Matheja, "Relatively Complete Verification of Probabilistic Programs" CoRR, vol. abs/2010.14548. 2020.

V. Astrauskas, C. Matheja, F. Poli, P. Müller, and A. J. Summers, "How do programmers use unsafe rust?" Proc. ACM Program. Lang. vol. 4, iss. OOPSLA. 2020.
doi: 10.1145/3428204

B. L. Kaminski, J. -, and C. Matheja, Expected Runtime Analyis by Program VerificationCambridge University Press. 2020.
doi: 10.1017/9781108770750.007

K. Batz, S. Junges, B. L. Kaminski, J. -, C. Matheja, and P. Schröer, "PrIC3: Property Directed Reachability for MDPs" in Proc. Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, 2020.
doi: 10.1007/978-3-030-53291-8_27

A. Aguirre, G. Barthe, J. Hsu, B. L. Kaminski, J. -, and C. Matheja, "Kantorovich Continuity of Probabilistic Programs" CoRR, vol. abs/1901.06540. 2019.

B. L. Kaminski, J. -, and C. Matheja, "On the hardness of analyzing probabilistic programs" Acta Informatica, vol. 56, iss. 3. 2019.
doi: 10.1007/S00236-018-0321-1

K. Batz, B. L. Kaminski, J. -, C. Matheja, and T. Noll, "Quantitative separation logic: a logic for reasoning about probabilistic pointer programs" Proc. ACM Program. Lang. vol. 3, iss. POPL. 2019.
doi: 10.1145/3290347

J. Katelaan, C. Matheja, and F. Zuleger, "Effective Entailment Checking for Separation Logic with Inductive Definitions" in Proc. Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II, 2019.
doi: 10.1007/978-3-030-17465-1_18

M. Sighireanu, J. A. N. Pérez, A. Rybalchenko, N. Gorogiannis, R. Iosif, A. Reynolds, C. Serban, J. Katelaan, C. Matheja, T. Noll, F. Zuleger, W. -, Q. L. Le, Q. -, T. -, T. -, S. -, M. Cyprian, A. Rogalewicz, T. Vojnar, C. Enea, O. Lengál, C. Gao, and Z. Wu, "SL-COMP: Competition of Solvers for Separation Logic" in Proc. Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, 2019.
doi: 10.1007/978-3-030-17502-3_8

K. Batz, B. L. Kaminski, J. -, and C. Matheja, "How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times" CoRR, vol. abs/1802.10433. 2018.

K. Batz, B. L. Kaminski, J. -, C. Matheja, and T. Noll, "Quantitative Separation Logic" CoRR, vol. abs/1802.10467. 2018.

B. L. Kaminski, J. -, C. Matheja, and F. Olmedo, "Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms" J. ACM, vol. 65, iss. 5. 2018.
doi: 10.1145/3208102

H. Arndt, C. Jansen, J. -, C. Matheja, and T. Noll, "Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs" in Proc. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, 2018.
doi: 10.1007/978-3-319-96142-2_1

K. Batz, B. L. Kaminski, J. -, and C. Matheja, "How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times" in Proc. Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, 2018.
doi: 10.1007/978-3-319-89884-1_7

J. Katelaan, C. Matheja, T. Noll, and F. Zuleger, "Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic" in Proc. LPAR-22 Workshop and Short Paper Proceedings, Awassa, Ethiopia, 16-21 November 2018, 2018.
doi: 10.29007/QWD8

H. Arndt, C. Jansen, C. Matheja, and T. Noll, "Graph-Based Shape Analysis Beyond Context-Freeness" in Proc. Software Engineering and Formal Methods - 16th International Conference, SEFM 2018, Held as Part of STAF 2018, Toulouse, France, June 27-29, 2018, Proceedings, 2018.
doi: 10.1007/978-3-319-92970-5_17

M. van Keulen, B. L. Kaminski, C. Matheja, and J. -, "Rule-Based Conditioning of Probabilistic Data" in Proc. Scalable Uncertainty Management - 12th International Conference, SUM 2018, Milan, Italy, October 3-5, 2018, Proceedings, 2018.
doi: 10.1007/978-3-030-00461-3_20

H. Arndt, C. Jansen, C. Matheja, and T. Noll, "Heap Abstraction Beyond Context-Freeness" CoRR, vol. abs/1705.03754. 2017.

C. Jansen, J. Katelaan, C. Matheja, T. Noll, and F. Zuleger, "Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic" in Proc. Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, 2017.
doi: 10.1007/978-3-662-54434-1_23

C. Jansen, J. Katelaan, C. Matheja, T. Noll, and F. Zuleger, "Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic" CoRR, vol. abs/1610.07041. 2016.

B. L. Kaminski, J. -, and C. Matheja, "Inferring Covariances for Probabilistic Programs" CoRR, vol. abs/1606.08280. 2016.

B. L. Kaminski, J. -, C. Matheja, and F. Olmedo, "Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs" CoRR, vol. abs/1601.01001. 2016.

F. Olmedo, B. L. Kaminski, J. -, and C. Matheja, "Reasoning about Recursive Probabilistic Programs" CoRR, vol. abs/1603.02922. 2016.

F. Olmedo, B. L. Kaminski, J. -, and C. Matheja, "Reasoning about Recursive Probabilistic Programs" in Proc. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, 2016.
doi: 10.1145/2933575.2935317

B. L. Kaminski, J. -, C. Matheja, and F. Olmedo, "Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs" in Proc. Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, 2016.
doi: 10.1007/978-3-662-49498-1_15

B. L. Kaminski, J. -, and C. Matheja, "Inferring Covariances for Probabilistic Programs" in Proc. Quantitative Evaluation of Systems - 13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings, 2016.
doi: 10.1007/978-3-319-43425-4_14

C. Matheja, C. Jansen, and T. Noll, "Tree-Like Grammars and Separation Logic" in Proc. Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings, 2015.
doi: 10.1007/978-3-319-26529-2_6