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

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

M. Kuhn, J. Grüger, C. Matheja, und 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. -, und 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

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

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

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

C. Matheja, J. Pagel, und 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.
doi: 10.1145/3534927

P. Schröer, K. Batz, B. L. Kaminski, J. -, und 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. -, und 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, und T. Noll, "Foundations for Entailment Checking in Quantitative Separation Logic (extended version)" CoRR, vol. abs/2201.11464.

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

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

K. Batz, I. Fesefeldt, M. Jansen, J. -, F. Keßler, C. Matheja, und 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, und 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, und P. Schröer, "Latticed k-Induction with an Application to Probabilistic Programs" CoRR, vol. abs/2105.14100.

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

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

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

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

K. Batz, M. Chen, B. L. Kaminski, J. -, C. Matheja, und 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, und 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, und F. Zuleger, "Complete Entailment Checking for Separation Logic with Inductive Definitions" CoRR, vol. abs/2002.01202.

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

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

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

K. Batz, S. Junges, B. L. Kaminski, J. -, C. Matheja, und 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. -, und C. Matheja, "Kantorovich Continuity of Probabilistic Programs" CoRR, vol. abs/1901.06540.

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

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

J. Katelaan, C. Matheja, und 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, und 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. -, und C. Matheja, "How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times" CoRR, vol. abs/1802.10433.

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

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

H. Arndt, C. Jansen, J. -, C. Matheja, und 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. -, und 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, und 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, und 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, und 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, und T. Noll, "Heap Abstraction Beyond Context-Freeness" CoRR, vol. abs/1705.03754.

C. Jansen, J. Katelaan, C. Matheja, T. Noll, und 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, und F. Zuleger, "Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic" CoRR, vol. abs/1610.07041.

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

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

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

F. Olmedo, B. L. Kaminski, J. -, und 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, und 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. -, und 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, und 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