Publications

See also DBLP or Google Scholar.

1

Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. A deductive verification infrastructure for probabilistic programs. Proc. ACM Program. Lang., (OOPSLA), to appear.

2

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht. A calculus for amortized expected runtimes. Proc. ACM Program. Lang., 7(POPL):1957–1986, 2023.

3

Christoph Matheja, Jens Pagel, and Florian Zuleger. A decision procedure for guarded separation logic complete entailment checking for separation logic with inductive definitions. ACM Trans. Comput. Log., 24(1):1:1–1:76, 2023.

4

Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Probabilistic program verification via inductive synthesis of inductive invariants. In TACAS (2), volume 13994 of Lecture Notes in Computer Science, 410–429. Springer, 2023.

5

Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. A deductive verification infrastructure for probabilistic programs. CoRR, 2023.

6

Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, and Thomas Noll. Foundations for entailment checking in quantitative separation logic. In ESOP, volume 13240 of Lecture Notes in Computer Science, 57–84. Springer, 2022.

7

Vytautas Astrauskas, Aurel B\'ılý, Jonás Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, and Alexander J. Summers. The prusti project: formal verification for rust. In NFM, volume 13260 of Lecture Notes in Computer Science, 88–108. Springer, 2022.

8

Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, and Thomas Noll. Foundations for entailment checking in quantitative separation logic (extended version). CoRR, 2022.

9

Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Probabilistic program verification via inductive synthesis of inductive invariants. CoRR, 2022.

10

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht. A calculus for amortized expected runtimes. CoRR, 2022.

11

Fabian Wolff, Aurel B\'ılý, Christoph Matheja, Peter Müller, and Alexander J. Summers. Modular specification and verification of closures in rust. Proc. ACM Program. Lang., 5(OOPSLA):1–29, 2021.

12

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. A pre-expectation calculus for probabilistic sensitivity. Proc. ACM Program. Lang., 5(POPL):1–28, 2021.

13

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

14

Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schröer. Latticed k-induction with an application to probabilistic programs. In CAV (2), volume 12760 of Lecture Notes in Computer Science, 524–549. Springer, 2021.

15

Ira Fesefeldt, Christoph Matheja, Thomas Noll, and Johannes Schulte. Automated checking and completion of backward confluence for hyperedge replacement grammars. In ICGT, volume 12741 of Lecture Notes in Computer Science, 283–293. Springer, 2021.

16

Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schröer. Latticed k-induction with an application to probabilistic programs. CoRR, 2021.

17

Aurel B\'ılý, Christoph Matheja, and Peter Müller. Flexible refinement proofs in separation logic. CoRR, 2021.

18

Christoph Matheja. Automated reasoning and randomization in separation logic. PhD thesis, RWTH Aachen University, Germany, 2020.

19

Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, and Alexander J. Summers. How do programmers use unsafe rust? Proc. ACM Program. Lang., 4(OOPSLA):136:1–136:27, 2020.

20

Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schröer. Pric3: property directed reachability for mdps. In CAV (2), volume 12225 of Lecture Notes in Computer Science, 512–538. Springer, 2020.

21

Jens Pagel, Christoph Matheja, and Florian Zuleger. Complete entailment checking for separation logic with inductive definitions. CoRR, 2020.

22

Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schröer. Pric3: property directed reachability for mdps. CoRR, 2020.

23

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Relatively complete verification of probabilistic programs. CoRR, 2020.

24

Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. On the hardness of analyzing probabilistic programs. Acta Informatica, 56(3):255–285, 2019.

25

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. Proc. ACM Program. Lang., 3(POPL):34:1–34:29, 2019.

26

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, and Zhilin Wu. SL-COMP: competition of solvers for separation logic. In TACAS (3), volume 11429 of Lecture Notes in Computer Science, 116–132. Springer, 2019.

27

Jens Katelaan, Christoph Matheja, and Florian Zuleger. Effective entailment checking for separation logic with inductive definitions. In TACAS (2), volume 11428 of Lecture Notes in Computer Science, 319–336. Springer, 2019.

28

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Kantorovich continuity of probabilistic programs. CoRR, 2019.

29

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM, 65(5):30:1–30:68, 2018.

30

Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. Let this graph be your witness! - an attestor for verifying java pointer programs. In CAV (2), volume 10982 of Lecture Notes in Computer Science, 3–11. Springer, 2018.

31

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. How long, O bayesian network, will I sample thee? - A program analysis perspective on expected sampling times. In ESOP, volume 10801 of Lecture Notes in Computer Science, 186–213. Springer, 2018.

32

Jens Katelaan, Christoph Matheja, Thomas Noll, and Florian Zuleger. Harrsh: A tool for unied reasoning about symbolic-heap separation logic. In LPAR (Workshop and Short Papers), volume 9 of Kalpa Publications in Computing, 23–36. EasyChair, 2018.

33

Hannah Arndt, Christina Jansen, Christoph Matheja, and Thomas Noll. Graph-based shape analysis beyond context-freeness. In SEFM, volume 10886 of Lecture Notes in Computer Science, 271–286. Springer, 2018.

34

Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, and Joost-Pieter Katoen. Rule-based conditioning of probabilistic data. In SUM, volume 11142 of Lecture Notes in Computer Science, 290–305. Springer, 2018.

35

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. How long, O bayesian network, will I sample thee? A program analysis perspective on expected sampling times. CoRR, 2018.

36

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. Quantitative separation logic. CoRR, 2018.

37

Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, and Florian Zuleger. Unified reasoning about robustness properties of symbolic-heap separation logic. In ESOP, volume 10201 of Lecture Notes in Computer Science, 611–638. Springer, 2017.

38

Hannah Arndt, Christina Jansen, Christoph Matheja, and Thomas Noll. Heap abstraction beyond context-freeness. CoRR, 2017.

39

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. Weakest precondition reasoning for expected run-times of probabilistic programs. In ESOP, volume 9632 of Lecture Notes in Computer Science, 364–389. Springer, 2016.

40

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Reasoning about recursive probabilistic programs. In LICS, 672–681. ACM, 2016.

41

Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Inferring covariances for probabilistic programs. In QEST, volume 9826 of Lecture Notes in Computer Science, 191–206. Springer, 2016.

42

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. Weakest precondition reasoning for expected run-times of probabilistic programs. CoRR, 2016.

43

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Reasoning about recursive probabilistic programs. CoRR, 2016.

44

Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Inferring covariances for probabilistic programs. CoRR, 2016.

45

Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, and Florian Zuleger. Unified reasoning about robustness properties of symbolic-heap separation logic. CoRR, 2016.

46

Christoph Matheja, Christina Jansen, and Thomas Noll. Tree-like grammars and separation logic. In APLAS, volume 9458 of Lecture Notes in Computer Science, 90–108. Springer, 2015.