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

Ahornstraße 55

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

## Research

I am a Ph.D. student at the Software Modeling and Verification Group (MOVES) headed by Professor Joost-Pieter Katoen involved in the Automated Probabilistic Program Analysis (APPA) project funded by the Excellence Initiative of the German federal and state government. From November 2016 till April 2017 I was visiting Alexandra Silva at the Programming Principles, Logic and Verification Group (PPLV) at University College London (UCL) for a four month period.

I am a collegiate and member of the steering committee of the DFG Research Training Group (DFG-Graduiertenkolleg) Uncertainty and Randomness in Algorithms, Verification, and Logic (UnRAVeL). I have previously been a collegiate of the DFG Research Training Group Algorithmic synthesis of reactive and discrete-continuous systems (AlgoSyn).

My fields of research interests include

- semantics of probabilistic programs,
- formal verification of probabilistic programs,
- 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.

### Program Committees & External Reviewing

I am serving on the Program Committee of the 16th International Conference on Quantitative on Quantitative Evaluation of SysTems (QEST 2019).

I have served on the Program Committee of the *15th International Conference on Quantitative Evaluation of SysTems* (QEST 2018)*,* part of CONFESTA 2018.

I was an external reviewer for ATVA 2017, CAV (2016, 2015), CONCUR 2018, LATA 2016, LICS (2017, 2018), Petri Nets 2016, POPL 2017, TACAS 2017, and Transactions on Computational Logic (TOCL).

### Open Topics for Theses

I always look forward to conduct research together with students! If you are interested in writing your thesis in the field of semantics or verification of probabilistic programs, or computability in connection with probabilities, I would be more than glad to hear from you!

Find further open topics for theses at our chair here.

### Supervision

Together with Christoph Matheja I have supervised our student research assistant Kevin Batz. Furthermore, I currently supervise the following thesis or internship projects:

- Lutz Klinkenberg.
*TBT.*Master’s thesis. - Kevin Batz.
*TBT.*Master’s thesis. (together with Sebastian Junges and Christoph Matheja) - Sonja Skiba.
*TBT.*Bacherlor’s thesis. - David Herzkamp.
*TBT.*Bachelor’s thesis.

In the past, I have been supervising the following theses:

- Joshua Peignier (ENS Rennes).
*Possibility Distribution Semantics for Probabilistic Programs with Nondeterminism*. Internship project. (together with Christoph Matheja) - Sven Deserno,
*Probabilistic Model Checking for Markov Chain Families.*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*

## Teaching

I am currently involved in the following teaching activities:

- Static Methods for Quantitative Program Analysis (Seminar)
- Algorithms and Data Structures (Proseminar)

Past teaching activities:

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

## Other Activities

I am a member of the Teaching Committee (Kommission für Lehre) of the Department of Computer Science at RWTH Aachen University (since 2014).

I am a member of a search committee for a full professorship in the field of *Machine Learning* (Berufungskommission für W3 Professur *Maschinelles Lernen*). In the past, I have been a member of two other search committees for full professorships, one of them an Alexander von Humboldt professorship.

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.

## Awards

- 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 Medal in 2014 for receiving a master’s degree with distinction.

## Selected Talks

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

2019 | |
---|---|

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic. POPL, to appear, 2019. | |

2018 | |

Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. Rule-based Conditioning of Probabilistic Data Integration. Proc. of the 12th International Conference on Scalable Uncertainty Management (SUM 2018), Volume of LNAI, 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. | |

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the Hardness of Analyzing Probabilistic Programs. Acta Informatica [to appear], 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. | |

Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen. A New Proof Rule for Almost-Sure Termination. Principles of Programming Languages (POPL), Volume of Proceedings of the ACM, ACM, . |