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

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.

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

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

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

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

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

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

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

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

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, 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, 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

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

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

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

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.

C. Matheja, "Automated reasoning and randomization in separation logic" PhD Thesis , 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

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

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

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.

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

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

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

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. -, 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

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.

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

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

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

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. -, 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

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.

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

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.

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