- benjamin.kaminski at cs.rwth-aachen.de
- Address
- Room 4230

Ahornstraße 55

D-52074 Aachen - Phone
- +49 241 80 21208

I am a postdoctoral researcher at the Software Modeling and Verification Group (MOVES) headed by Professor Prof. Joost-Pieter Katoen associated with the DFG Research Training Group (DFG-Graduiertenkolleg) Uncertainty and Randomness in Algorithms, Verification, and Logic (UnRAVeL). Previously, I was a collegiate with UnRAVeL and a member of its steering committee.

From November 2016 till April 2017 I was visiting Prof. Alexandra Silva at the Programming Principles, Logic and Verification Group (PPLV) at University College London (UCL) for a four month period, where I worked on Angluin-style learning of probabilistic automata.

In the beginning of my PhD, I was involved in the Automated Probabilistic Program Analysis (APPA) project funded by the Excellence Initiative of the German federal and state government and a collegiate of the DFG Research Training Group Algorithmic synthesis of reactive and discrete-continuous systems (AlgoSyn).

# Thesis

In February 2019, I have defended my PhD thesis titled *Advanced Weakest Precondition Calculi for Probabilistic Programs*. Please find more information on my thesis, including a PDF version, by clicking the cover on the right.

The thesis gives a comprehensive introduction to weakest preexpectation reasoning and features (amongst others) calculi for verifying expected runtimes and probabilistic programs with conditioning. A Special focus is put on inductive proof rules for reasoning about loops.

# Research

My research interests include

- semantics and formal verification of probabilistic programs,
- quantitative verification techniques,
- verification of non-functional requirements,
- machine learning and verification,
- explainable verification,
- recursion theory, and
- (mathematical) logic.

For a list of publications and a list of selected talks, see the bottom of this page.

You can also find me on dblp and Google Scholar.

## Students

I am currently supervising my student research assistant Lena Verscht. Together with Christoph Matheja I have supervised our student research assistant Kevin Batz. Furthermore, I have supervised the following thesis and internship projects:

- Lena Verscht.
*Weakest Preexpectation Reasoning for Amortized Expected Runtimes*. Bachelor’s Thesis. - Lutz Klinkenberg.
*On Probability Generating Functions for Program Analysis*. Master’s thesis. - Kevin Batz.
*IC3 for Probabilistic Systems*. Master’s thesis. (together with Sebastian Junges and Christoph Matheja) - Sonja Skiba.
*Towards Completeness of a Proof Rule for Almost-sure Termination*. Bacherlor’s thesis. - David Herzkamp.
*Hardness of Probabilistic Termination with Nondeterminism.*Bachelor’s thesis. - Joshua Peignier (ENS Rennes).
*Possibility Distribution Semantics for Probabilistic Programs with Nondeterminism*. 2017. Internship project. (together with Christoph Matheja) - Sven Deserno,
*Probabilistic Model Checking for Markov Chain Families.*2017. Master’s thesis. (together with Sebastian Junges) - Kevin Batz.
*Proof Rules for Expected Run-Times of Probabilistic Programs.*2017. Bachelor’s thesis. (together with Christoph Matheja). - Simon Feiden.
*Extending Probability Generating Function Semantics to Negative Variable Valuations.*2016. Bachelor’s thesis. - Clara Scherbaum.
*Probability Generating Function Semantics for Probabilistic Programs.*2016. Bachelor’s thesis. (winner of thefor outstanding bachelor theses)*itestra innovation Award*

## Peer Review

### Program Committees

*16th International Conference on Quantitative Evaluation of SysTems*(QEST 2019)*15th International Conference on Quantitative Evaluation of SysTems*(QEST 2018)*,*part of CONFESTA 2018

### External Reviewer

#### Research Funding Proposals

#### Edited Volumes

#### Journals

- Transactions on Computational Logic (TOCL)
- Transactions on Programming Languages and Systems (TOPLAS)

#### Conferences

# Teaching

- Formale Systeme, Automaten, Prozesse (SS 19)
- Foundations of Probabilistic Programming (SS 19)
- Static Methods for Quantitative Program Analysis (Seminar)
- Formal Verification Meets Machine Learning (Seminar)
- Datenstrukturen und Algorithmen (SS 18)
- Semantics and Verification of Software
- Foundations of Probabilistic Programming (Seminar)
- Verification and Static Analysis of Software (Seminar) (SS 17)
- Vorkurs Informatik (Diskrete Mathematik) (SS 16, SS 15, SS 14)
- Theoretical Foundations of the UML (SS 16)
- Probabilistic Programming (Seminar) (SS 16)
- Concurrency Theory (WS 15/16, WS 13/14)
- Algorithms and Data Structures (Proseminar) (WS 18/19, WS 15/16, WS 13/14)
- Datenstrukturen und Algorithmen (SS 15)
- Principles of Programming Languages (Seminar) (SS 15)
- Static Program Analysis (WS 14/15)
- Probabilistic Programs (Seminar) (WS 14/15)
- Turing Award Topics (Proseminar) (WS 14/15)
- Modeling and Verification of Probabilistic Systems (SS 14)
- Concurrency Theory (Seminar) (SS 14)

# Awards

- I was a selected attendee of the 7th Heidelberg Laureate Forum.
- Our paper
*Rule-based Conditioning of Probabilistic Data*(joint work with Maurice van Keulen, Christoph Matheja and Joost-Pieter Katoen) won the Best Paper Award at SUM 2018. The paper presents how to integrate evidences into a probabilistic database by means of conditioning. - Our paper
*How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times*(joint work with Kevin Batz, Joost-Pieter Katoen, and Christoph Matheja) was nominated for the EATCS Best Paper Award at ETAPS 2018. The paper shows how to use deductive program verification to deduce the expected time to obtain a single i.i.d-sample from a Bayesian network when using rejection sampling. The approach has been automated and shows that determining expected sampling times of the order of millions years for large BNs can be done in a matter of seconds. - I was awarded the LMW 2017 Scholarship by ACM SIGLOG in 2017.
- I was awarded the FITweltweit scholarship by the German Academic Exchange Service (DAAD) in 2016.
- Our paper
*Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs*(joint work with Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo) won the EATCS Best Paper Award for the best theory paper presented at ETAPS 2016. The paper presents a wp-style calculus for probabilistic programs to analyze their expected runtimes, together with a set of proof rules for loops, and shows its application to several examples, including the coupon collector’s problem. Find a picture of the four happy award winners here. - My colleague Christian Dehnert and I were nominated for the Teaching Award 2015 awarded by the student body of the Faculty of Mathematics, Computer Science and Natural Sciences. The winner of the award was Wied Pakusa whom I was more than lucky to have as a tutor when I was an undergraduate student.
- I was awarded the Springorum Commemorative Coin in 2014 for receiving a master’s degree with distinction.

# Other Activities

I was a member of the Teaching Committee (Kommission für Lehre) of the Department of Computer Science at RWTH Aachen University from 2014 till 2018.

I was a member of several search committees for full professorships (W2 and W3, including an Alexander von Humboldt professorship) in the fields of *Neural Computing*, *Machine Learning*, and *Data Science*.

I gave several popular scientific talks for interested high school students, e.g. at Aachener Informatiktage 2014, Erstinfotag 2014, or Beratungstage 2018.

I participated in the BeBuddy program of RWTH’s International Office.

# Selected Talks

2019 | |
---|---|

Benjamin Lucien Kaminski. Reasoning about Expected Runtimes of Probabilistic Programs (and Quantitative Separation Logic), Talk at Schloss Dagstuhl, 2019. | |

Benjamin Lucien Kaminski. Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs, Talk at Highlights of Logic, Games and Automata, 2019. | |

Benjamin Lucien Kaminski. Advanced Weakest Precondition Calculi for Probabilistic Programs, Talk at PhD Defense, Aachen, 2019. | |

2018 | |

Benjamin Lucien Kaminski. Quantitative Separation Logic, Talk at UnRAVeL Seminar, RWTH Aachen, 2018. | |

Benjamin Lucien Kaminski. How long, O Bayesian network, will I sample thee?, Talk at 27th European Symposium on Programming (ESOP 2018), Thessaloniki, Greece, 2018. | |

2017 | |

Benjamin Lucien Kaminski. Proving Almost-Sure Termination with Non-Ranking Supermartingales, Talk at ROCKS Meeting, Münster, Germany, 2017. | |

Benjamin Lucien Kaminski. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations, Talk at 2nd Workshop on Probabilistic Programming Semantics (PPS 2017), Paris, France, 2017. | |

Benjamin Lucien Kaminski. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations, Talk at 32nd Annual Symposium on Logic in Computer Science (LICS 2017), Reykjavik, Iceland, 2017. | |

Benjamin Lucien Kaminski. Reasoning about Expected Run-Times of Probabilistic Programs, Talk at Oxford Verification Seminar, University of Oxford, United Kingdom, 2017. | |

Benjamin Lucien Kaminski. Reasoning about Expected Run-Times of Probabilistic Programs, Talk at 5th Southern-Region English Programming Language Seminar (S-REPLS 5), Oxford, United Kingdom, 2017. | |

Benjamin Lucien Kaminski. Tutorial on Weakest Precondition Reasoning for Probabilistic Programs and Presentation of a Weakest Pre-Expectation Semantics for Mixed-Sign Expectations, Talk at Programming Principles, Logic and Verification Seminar, University College London, United Kingdom, 2017. | |

2016 | |

Benjamin Lucien Kaminski. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations, Talk at Working Seminar on Formal Models, Discrete Structures, and Algorithms, Masaryk University, Brno, Czech Republic, 2016. | |

Benjamin Lucien Kaminski. Expected Run-Times of Probabilistic Programs, Talk at Research Program on Automata, Logic and Games organized by the Institute for Mathematical Sciences at National University of Singapore, 2016. | |

Benjamin Lucien Kaminski. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs, Talk at 25th European Symposium on Programming (ESOP 2016), Eindhoven, The Netherlands, 2016. | |

2015 | |

Benjamin Lucien Kaminski. Probabilistic Programs - A Natural Model for Approximate Computations, Talk at Workshop on Approximate Computing (AC15), Paderborn, Germany, 2015. | |

Benjamin Lucien Kaminski. On the Hardness of Almost-Sure Termination, Talk at 40th International Symposium on Mathematical Foundations of Computer Science (MFCS 2015), Milan, Italy, 2015. | |

Benjamin Lucien Kaminski. Conditioning in Probabilistic Programming, Talk at 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS 2015), Nijmegen, The Netherlands, 2015. | |

Benjamin Lucien Kaminski. On the Hardness of Almost-Sure Termination, Talk at Dagstuhl Seminar "Challenges and Trends in Probabilistic Programming", Schloss Dagstuhl, Germany, 2015. | |

Benjamin Lucien Kaminski. Analyzing Expected Outcomes and (Positive) Almost-Sure Termination of Probabilistic Programs is Hard, Talk at Young Researchers' Conference "Frontiers of Formal Methods" (FFM), Aachen, Germany, 2015. | |

2014 | |

Benjamin Lucien Kaminski. Analyzing Expected Outcomes and Almost-Sure Termination of Probabilistic Programs is Hard, Talk at AlgoSyn, RWTH Aachen, Germany, 2014. |

## Publications for Benjamin Lucien Kaminski

2020 | |
---|---|

Marcel Hark, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Jürgen Giesl. Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification. Proceedings of the ACM on Programming Languages [to appear], 2020. | |

2019 | |

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the Hardness of Analyzing Probabilistic Programs. Acta Informatica 56(3), pages 255-285, 2019. | |

Benjamin Lucien Kaminski. Advanced Weakest Precondition Calculi for Probabilistic Programs. Phd Thesis at RWTH Aachen University, 2019. | |

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic. Proceedings of the ACM on Programming Languages 3(POPL), pages 34:1-34:29, 2019. | |

2018 | |

Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. Rule-based Conditioning of Probabilistic Data Integration (Best Paper Award). Proc. of the 12th International Conference on Scalable Uncertainty Management (SUM 2018), Volume 11142 of LNAI, pages 290-305, Springer, 2018. | |

Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. A Program Analysis Perspective on Expected Sampling Times. Collected Abstracts of the 1st International Conference on Probabilistic Programming (PROBPROG 2018), 2018. | |

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. Journal of the ACM 65(5), pages 30:1-30:68, 2018. | |

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times.. Proc. of the 27th European Symposium on Programming (ESOP 2018), Volume 10801 of LNCS, pages 186-213, Springer, 2018. | |

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic. Technical report at arxiv number 1802.10467, 2018. | |

Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver. Conditioning in Probabilistic Programming. ACM Transactions on Programming Languages and Systems (TOPLAS) 40(1), pages 4:1-4:50, 2018. | |

Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen. A New Proof Rule for Almost-Sure Termination. Proc. of the 45th Symposium on Principles of Programming Languages (POPL 2018), pages 33:1-33:28, 2018. | |

2017 | |

Benjamin Lucien Kaminski, Joost-Pieter Katoen. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations. Proc. of the 32nd Annual Symposium on Logic in Computer Science (LICS 2017), pages 1-12, IEEE, 2017. | |

Benjamin Lucien Kaminski, Joost-Pieter Katoen. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations. Collected Abstracts of the 2nd Workshop on Probabilistic Programming Semantics (PPS 2017), 2017. | |

2016 | |

Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen. Bounded Model Checking for Probabilistic Programs. Proc. of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), Volume 9938 of LNCS, Springer, 2016. | |

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Inferring Covariances for Probabilistic Programs. Proc. of the 13th International Conference on Quantitative Evaluation of SysTems (QEST 2016), Volume 9826 of LNCS, pages 191-206, Springer, 2016. | |

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Reasoning about Recursive Probabilistic Programs. Proc. of the 31st Annual Symposium on Logic in Computer Science (LICS 2016), pages 672-681, ACM, 2016. | |

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs (EATCS Best Paper Award). Proc. of the 25th European Symposium on Programming (ESOP 2016), Volume 9632 of LNCS, pages 364 - 389, Springer, 2016. | |

Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo. On the Semantic Intricacies of Conditioning. Collected Abstracts of the 1st Workshop on Probabilistic Programming Semantics (PPS 2016), 2016. | |

2015 | |

Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Probabilistic Programs - A Natural Model for Approximate Computations. Workshop on Approximate Computing (AC15), 2015. | |

Joost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Federico Olmedo. Understanding Probabilistic Programs. Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Volume 9360 of LNCS, pages 15-32, Springer, 2015. | |

Benjamin Lucien Kaminski, Joost-Pieter Katoen. On the Hardness of Almost-Sure Termination. Proc. of the 40th International Symposium on Mathematical Foundations of Computer Science (MFCS 2015), Part I, Volume 9234 of LNCS, pages 307-318, Springer, 2015. | |

Benjamin Lucien Kaminski. Analyzing Expected Outcomes and (Positive) Almost-Sure Termination of Probabilistic Programs is Hard. Proc. of the Young Researchers' Conference "Frontiers of Formal Methods" (FFM 2015), pages 179-184, Aachener Informatik Berichte, 2015. | |

Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo, Friedrich Gretz, Annabelle McIver. Conditioning in Probabilistic Programming. Proc. of the 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS 2015), ENTCS 319, pages 199-216, 2015. | |

2011 | |

Raimondas Sasnauskas, Oscar Soria Dustmann, Benjamin Lucien Kaminski, Klaus Wehrle, Carsten Weise, Stefan Kowalewski. Scalable Symbolic Execution of Distributed Systems. Proc. of the 31st International Conference on Distributed Computing Systems (ICDCS 2011), pages 333-342, IEEE Computer Society, 2011. |