Benjamin Kaminski

kaminski2

Email
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 KlinkenbergOn 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 BatzProof 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 ScherbaumProbability Generating Function Semantics for Probabilistic Programs. 2016. Bachelor’s thesis. (winner of the itestra innovation Award for outstanding bachelor theses)

Peer Review

Program Committees

External Reviewer

Research Funding Proposals

Edited Volumes

Journals

Conferences

Teaching

Awards

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 2014Erstinfotag 2014, or Beratungstage 2018.

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

Selected Talks

2019
DownloadLinkBenjamin Lucien Kaminski. Reasoning about Expected Runtimes of Probabilistic Programs (and Quantitative Separation Logic), Talk at Schloss Dagstuhl, 2019.
DownloadLinkBenjamin Lucien Kaminski. Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs, Talk at Highlights of Logic, Games and Automata, 2019.
DownloadLinkBenjamin 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.
DownloadLinkBenjamin Lucien Kaminski. How long, O Bayesian network, will I sample thee?, Talk at 27th European Symposium on Programming (ESOP 2018), Thessaloniki, Greece, 2018.
2017
DownloadLinkBenjamin 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.
DownloadLinkBenjamin 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.
DownloadLinkBenjamin 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.
DownloadLinkBenjamin 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.
DownloadLinkBenjamin 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.
DownloadLinkBenjamin 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
DownloadLinkBenjamin 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
DOIDownloadLinkBenjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the Hardness of Analyzing Probabilistic Programs. Acta Informatica 56(3), pages 255-285, 2019.
DownloadLinkBenjamin Lucien Kaminski. Advanced Weakest Precondition Calculi for Probabilistic Programs. Phd Thesis at RWTH Aachen University, 2019.
DOIKevin 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
DOIMaurice 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.
DOIBenjamin 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.
DOIDownloadLinkKevin 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.
LinkKevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic. Technical report at arxiv number 1802.10467, 2018.
DOIFederico 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.
DOIAnnabelle 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
DOIBenjamin 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.
DownloadLinkBenjamin 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
DOIDownloadLinkNils 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.
DOIDownloadLinkBenjamin 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.
DOIDownloadLinkFederico 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.
DOIBenjamin 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
DownloadLinkNils 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.
DOIJoost-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.
DOIDownloadLinkBenjamin 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.
DownloadLinkBenjamin 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.
DOIDownloadLinkNils 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
DownloadLinkRaimondas 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.