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

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

Editorial Board Memberships

Program Committees

  • 33rd Int’l Conf. on Computer-Aided Verification (CAV 2021)
  • 31st Int’l Conf. on Concurrency Theory (CONCUR 2020), part of QONFEST 2020
  • 23rd Int’l Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR23) (2020)
  • 16th Int’l Conf. on Quantitative Evaluation of SysTems (QEST 2019)
  • 15th Int’l Conf. on Quantitative Evaluation of SysTems (QEST 2018), part of CONFESTA 2018

External Reviewer

Research Funding Proposals

  • Czech Science Foundation (GACR) (2019)

Edited Volumes

Journals

  • Mathematical Structures in Computer Science (MSCS) (2020)
  • Theoretical Computer Science (TCS) (2020)
  • Transactions on Computational Logic (TOCL) (2017)
  • Transactions on Modeling and Computer Simulation (TOMACS) (2020)
  • Transactions on Programming Languages and Systems (TOPLAS) (2019)

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.

2020
arXiv:2007.06327 [bibtex] [issue] Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Kevin Stefan Batz, Lutz Klinkenberg, Tobias Winkler. Generating Functions for Probabilistic Programs, 2020. https://arxiv.org/abs/2007.06327
DOI [bibtex] [issue] Benjamin Lucien Kaminski, Joost-Pieter Katoen, Martin Grohe, Peter Lindner. Generative Datalog with Continuous Distributions, 39th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2020), 347-360, ACM, 2020.
DOI [bibtex] [issue] Benjamin Lucien Kaminski, Joost-Pieter Katoen, Jürgen Giesl, Marcel Hark. Aiming low is harder, Proceedings of the ACM on programming languages 4 (POPL), pages 1-28, ACM, 2020.
2019
DOI fulltext PDF [bibtex] [issue] Benjamin Lucien Kaminski. Advanced weakest precondition calculi for probabilistic programs, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (xiv, 363 Seiten) : Illustrationen, Diagramme, 2019.
DOI fulltext PDF [bibtex] [issue] Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen, Kevin Batz, Thomas Noll. Quantitative separation logic, Proceedings of the ACM on programming languages 3 (POPL), pages 34, ACM, 2019.
DOI [bibtex] [issue] Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. On the hardness of analyzing probabilistic programs, Acta informatica 56 (3), pages 255–285, Springer, 2019.
2018
DOI [bibtex] [issue] Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen, Kevin Batz. How long, O Bayesian network, will I sample thee?, 27th European Symposium on Programming (ESOP 2018), LNCS, 186-213, Springer, 2018.
DOI [bibtex] [issue] Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen, Maurice van Keulen. Rule-Based Conditioning of Probabilistic Data, 12th International Conference on Scalable Uncertainty Management (SUM 2018), Volume 11142 of Lecture Notes in Artificial Intelligence, 290-305, Springer, 2018.
DOI [bibtex] [issue] Benjamin Lucien Kaminski, Christoph Matheja, Federico Olmedo, Joost-Pieter Katoen. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms, Journal of the ACM 65 (5), pages 30:1-30:68, 2018.
arXiv:1802.10467 [bibtex] [issue] Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen, Kevin Batz, Thomas Noll. Quantitative Separation Logic, 159 Seiten, 2018. https://arxiv.org/abs/1802.10467
DOI [bibtex] [issue] Annabelle McIver, Benjamin Lucien Kaminski, Carroll Morgan, Joost-Pieter Katoen. A new proof rule for almost-sure termination, Proceedings of the ACM on Programming Languages 2, pages 33:1-33:28, ACM, 2018.
DOI [bibtex] [issue] Annabelle Mciver, Benjamin Lucien Kaminski, Federico Olmedo, Friedrich Gretz, Joost-Pieter Katoen, Nils Jansen. Conditioning in Probabilistic Programming, ACM transactions on programming languages and systems 40 (1), pages 4, Association for Computing Machinery, 2018.
2017
[bibtex] [issue] Benjamin Lucien Kaminski, Joost-Pieter Katoen. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations, Symposium on Logic in Computer Science (LICS), 1-12, IEEE, 2017.
2016
DOI [bibtex] [issue] Benjamin Lucien Kaminski, Christoph Matheja, Federico Olmedo Beron, Joost-Pieter Katoen. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs, Volume 9632 of LNCS, 364-389, Springer, 2016.
fulltext PDF [bibtex] [issue] Benjamin Lucien Kaminski, Federico Olmedo Beron, Friedrich Gretz, Joost-Pieter Katoen, Nils Jansen. On the Semantic Intricacies of Conditioning, 2 Seiten, 2016.
DOI [bibtex] [issue] Benjamin Lucien Kaminski, Hans Christian Dehnert, Joost-Pieter Katoen, Lukas Westhofen, Nils Jansen. Bounded Model Checking for Probabilistic Programs, 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), Volume 9938 of LNCS, 68-85, Springer, 2016.
DOI [bibtex] [issue] Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. Inferring Covariances for Probabilistic Programs, 13th International Conference on Quantitative Evaluation of Systems (QEST 2016), Volume 9826 of LNCS, 191-206, Springer, 2016.
DOI [bibtex] [issue] Benjamin Lucien Kaminski, Christoph Matheja, Federico Olmedo Beron, Joost-Pieter Katoen. Reasoning about Recursive Probabilistic Programs, The 31st Annual ACM/IEEE Symposium, 672-681, ACM Press, 2016.
2015
DOI [bibtex] [issue] 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, 308-318, Springer, 2015.
[bibtex] [issue] Benjamin Lucien Kaminski, Christoph Matheja, Federico Olmedo, Joost-Pieter Katoen, Nils Jansen. Probabilistic Programs - A Natural Model for Approximate Computations, Workshop on Approximate Computing (AC15), 2015.
DOI [bibtex] [issue] Benjamin Lucien Kaminski, Federico Olmedo Beron, Friedrich Gretz, Joost-Pieter Katoen, Nils Jansen. Understanding Probabilistic Programs, Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Volume 9360 of LNCS, 15-32, Springer, 2015.
DOI fulltext PDF [bibtex] [issue] Annabelle McIver, Benjamin Lucien Kaminski, Federico Olmedo, Friedrich Gretz, Joost-Pieter Katoen, Nils Jansen. Conditioning in Probabilistic Programming, Electronic notes in theoretical computer science 319, pages 199-216, Elsevier Science, 2015.