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

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

- Sven Deserno,
*Probabilistic Model Checking for Markov Chain Families.*Master thesis. (together with Sebastian Junges) - 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 thefor outstanding bachelor theses)*itestra innovation Award*

### Reviewer

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

## Teaching

I am currently involved in the following teaching activities:

Past teaching activities:

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

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), [to appear], Volume of PACM, , 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. | |

Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver. Conditioning in Probabilistic Programming. In , ACM Transactions on Programming Languages and Systems (TOPLAS), [to appear], 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, . |

## Selected Talks

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