- benjamin.kaminski at cs.rwth-aachen.de
- Room 4230
- +49 241 80 21208
I am a Lecturer at the Programming Principles, Logic and Verification Group (PPLV) at University College London (UCL). New website is coming up soon(ish). For now, this site is kept up-to-date.
Before moving to UCL, I did my PhD here at the Software Modeling and Verification Group (MOVES) headed by Professor Prof. Joost-Pieter Katoen. I was associated with the DFG Research Training Group (DFG-Graduiertenkolleg) Uncertainty and Randomness in Algorithms, Verification, and Logic (UnRAVeL) and a member of its steering committee.
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.
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.
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 the itestra innovation Award for outstanding bachelor theses)
- 31st International Conference on Concurrency Theory (CONCUR 2020), part of QONFEST 2020
- 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR23, 2020)
- 16th International Conference on Quantitative Evaluation of SysTems (QEST 2019)
- 15th International Conference on Quantitative Evaluation of SysTems (QEST 2018), part of CONFESTA 2018
Research Funding Proposals
- Transactions on Computational Logic (TOCL) (2017)
- Transactions on Programming Languages and Systems (TOPLAS) (2019)
- 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)
- My colleagues Jera Hensel, Tim Quatmann, Matthias Volk, and I were nominated for the Teaching Award 2019 awarded by the student body of the Faculty of Mathematics, Computer Science and Natural Sciences.
- 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.
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 participated in the BeBuddy program of RWTH’s International Office.
|[bibtex]||Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs, Proceedings of the ACM on programming languages 3 (POPL), pages 34, 2019.|
|[bibtex]||Benjamin Lucien Kaminski. Advanced weakest precondition calculi for probabilistic programs, PhD Thesis, RWTH Aachen University, 363 pages, 2019.|
|[bibtex]||Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. Rule-Based Conditioning of Probabilistic Data, 12th International Conference on Scalable Uncertainty Management (SUM 2018), Volume 11142 of Lecture Notes in Artificial Intelligence, pages 290-305, Springer, 2018.|
|[bibtex]||Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the hardness of analyzing probabilistic programs, Acta informatica , 2018.|
|[bibtex]||Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, . Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms, Journal of the ACM : JACM 65 (5), pages 30:1-30:68, 2018.|
|[bibtex]||Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic : A Logic for Reasoning about Probabilistic Programs, 2018. arXiv:1802.10467|
|[bibtex]||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, 27th European Symposium on Programming (ESOP 2018), LNCS, pages 186-213, Springer, 2018.|
|[bibtex]||Benjamin Lucien Kaminski, Joost-Pieter Katoen. A new proof rule for almost-sure termination, Proceedings of the ACM on Programming Languages 2, pages 33:1-33:28, 2018., ,|
|[bibtex]||Benjamin Lucien Kaminski, Joost-Pieter Katoen, . Conditioning in Probabilistic Programming, ACM transactions on programming languages and systems : ACM TOPLAS 40 (1), pages 4, 2018., , ,|
|[bibtex]||Benjamin Lucien Kaminski, Joost-Pieter Katoen. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations, Symposium on Logic in Computer Science (LICS), pages 1-12, IEEE, 2017.|
|[bibtex]||Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Inferring Covariances for Probabilistic Programs, 13th International Conference on Quantitative Evaluation of Systems (QEST 2016), Volume 9826 of LNCS, pages 191-206, Springer, 2016.|
|[bibtex]||Federico Olmedo Beron, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Reasoning about Recursive Probabilistic Programs, The 31st Annual ACM/IEEE Symposium, pages 672-681, ACM Press, 2016.|
|[bibtex]||Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo Beron. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs, 25th European Symposium on Programming (ESOP 2016), Volume 9632 of LNCS, pages 364-389, Springer, 2016.|
|[bibtex]||Hans Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen. Bounded Model Checking for Probabilistic Programs, 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), Volume 9938 of LNCS, pages 68-85, Springer, 2016.,|
|[bibtex]||Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo Beron. On the Semantic Intricacies of Conditioning, 1st Workshop on Probabilistic Programming Semantics (PPS 2016), 2 pages, 2016.|
|[bibtex]||Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, , . Probabilistic Programs - A Natural Model for Approximate Computations, Workshop on Approximate Computing (AC15), 2015.|
|[bibtex]||Joost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Federico Olmedo Beron. Understanding Probabilistic Programs, Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Volume 9360 of LNCS, pages 15-32, Springer, 2015.|
|[bibtex]||Benjamin Lucien Kaminski, Joost-Pieter Katoen. On the Hardness of Almost–Sure Termination, 40th International Symposium on Mathematical Foundations of Computer Science (MFCS 2015), Volume 9234 of LNCS, pages 308-318, Springer, 2015.|
|[bibtex]||Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo, Friedrich Gretz, Annabelle McIver. Conditioning in Probabilistic Programming, Electronic notes in theoretical computer science 319, pages 199-216, 2015.|
|[bibtex]||Benjamin Lucien Kaminski, Wolfgang Marquardt, Lasse Greiner, Sebastian Heger, Kerstin Bluhm, Manuel Hechinger, Manuel Dahmen, Jakob Mottweiler, Dominique Dechambre, Henner Hollert, André Bardow, Carsten Bolm, Kai Leonhard, Ludger Wolfgang Michael Wolff. CIF-3 : Model-Based Fuel Design, TMFB 2nd International Conference, 2014.|
|[bibtex]||Raimondas Sasnauskas, Oscar Soria Dustmann, Benjamin Lucien Kaminski, Klaus Wehrle, Carsten Weise, Stefan Kowalewski. Scalable symbolic execution of distributed systems, 2011 31st International Conference on Distributed Computing Systems, (ICDCS 2011), pages 333-342, IEEE, 2011.|