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

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 was a collegiate of the DFG Research Training Group (DFG-Graduiertenkolleg) Algorithmic synthesis of reactive and discrete-continuous systems (AlgoSyn). My fields of interest include

  • semantics of probabilistic programs,
  • formal verification of probabilistic programs,
  • recursion theory, and
  • (mathematical) logic.

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

You can also find me on dblp and Google Scholar.

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 supervise our student research assistant Kevin Batz. Furthermore, I currently supervise the following thesis or internship projects:

  • Joshua Peignier (ENS Rennes), Possibility Distribution Semantics for Probabilistic Programs with Nondeterminism. Internship. (together with Christoph Matheja)
  • Sven Deserno, Probabilistic Model Checking for Markov Chain Families. Master thesis. (together with Sebastian Junges)

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

  • Kevin Batz, Proof Rules for Expected Run-Times of Probabilistic Programs. 2017. Bachelor thesis. (together with Christoph Matheja).
  • Simon Feiden, Extending Probability Generating Function Semantics to Negative Variable Valuations. 2016. Bachelor thesis.
  • Clara Scherbaum, Probability Generating Function Semantics for Probabilistic Programs. 2016. Bachelor thesis. (winner of the itestra innovation Award for outstanding bachelor theses)

Reviewer

I was an external reviewer for ATVA 2017CAV (20162015), LATA 2016LICS 2017PETRI NETS 2016POPL 2017TACAS 2017, and Transactions on Computational Logic (TOCL).

Teaching

I am currently involved in the following teaching activities:

Past teaching activities:

Other Activities

I am a member of two search committees for a professorship (Berufungskommission für Universitätsprofessur) and of the Teaching Committee (Kommission für Lehre) of the Department of Computer Science at RWTH Aachen University (since 2014).

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

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

Awards

I was awarded the FITweltweit scholarship by the German Academic Exchange Service (DAAD).

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 run-times, 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 for receiving a master’s degree with distinction.

Publications for Benjamin Lucien Kaminski

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), [to appear], 2017.
DownloadBenjamin 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
DownloadNils 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.
DownloadBenjamin 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.
DownloadFederico 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
DownloadNils 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.
DownloadBenjamin 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.
DownloadBenjamin 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.
DownloadNils 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
DownloadRaimondas 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.

Selected Talks

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.
DownloadBenjamin 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.
DownloadBenjamin 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.
DownloadBenjamin 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.
DownloadBenjamin 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
DownloadBenjamin Lucien Kaminski. Analyzing Expected Outcomes and Almost-Sure Termination of Probabilistic Programs is Hard, Talk at AlgoSyn, RWTH Aachen, Germany, 2014.