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 have moved to become a Professor at Saarland University.
My new website is here!
The website you are currently looking at is outdated.

I am also a Lecturer at the Programming Principles, Logic and Verification Group (PPLV) at University College London (UCL).

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.

Awards

Distinguished Paper Award at POPL 2021

Our paper A Pre-expectation Calculus for Probabilistic Sensitivity (joint work with Alejandro Aguirre, Gilles Barthe, Justin Hsu, Joost-Pieter Katoen, and Christoph Matheja) has received the Distinguished Paper Award at POPL 2021. The paper describes a weakest-precondition-style calculus for reasoning about relational properties and sensitivity of probabilistic programs. At most 10% of all accepted papers are designated as distinguished papers.

Best Paper Award at LOPSTR 2020

Our paper Generating Functions for Probabilistic Programs (joint work with Lutz Klinkenberg, Kevin Batz, Joost-Pieter Katoen, Joshua Moerman, and Tobias Winkler) has received the Best Paper Award at LOPSTR 2020. The paper describes how to employ probability generating functions in verification of probabilistic programs.

Ackermann Award 2020

My PhD Dissertation Advanced Weakest Precondition Calculi for Probabilistic Programs has been honored with the Ackermann Award 2020 of the EACSL. The Ackermann Award is awarded for outstanding dissertations in Computer Science Logic.

Nomination for Dissertation Award of the GI

My PhD Dissertation Advanced Weakest Precondition Calculi for Probabilistic Programs was nominated for the Dissertation Award of the German Informatics Society (GI). It was the single nomination out of all computer science dissertations defended in 2019 at RWTH Aachen.

Nomination for Teaching Award 2019

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.

Borchers Badge

I have been awarded the Borchers Badge in 2019 for receiving a Doctoral degree (PhD) with distinction.

Select Attendee of Heidelberg Laureate Forum

I was a selected attendee of the 7th Heidelberg Laureate Forum.

Best Paper Award at SUM 2018

Our paper Rule-based Conditioning of Probabilistic Data (joint work with Maurice van Keulen, Christoph Matheja and Joost-Pieter Katoen) has received the Best Paper Award at SUM 2018. The paper presents how to integrate evidences into a probabilistic database by means of conditioning.

Nomination for EATCS Best Paper Award at ETAPS (ESOP) 2018

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 of years for large BNs can be done in a matter of seconds.

LMW 2017 Scholarship

I was awarded the Logic Mentoring Workshop 2017 Scholarship by ACM SIGLOG in 2017.

FITweltweit Scholarship by the DAAD

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

EATCS Best Paper Award at ETAPS (ESOP) 2016

Our paper Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs (joint work with Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo) has received 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.

Nomination for Teaching Award 2015

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.

Springorum Commemorative Coin

I have been awarded the Springorum Commemorative Coin in 2014 for receiving a master’s degree with distinction.

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

Peer Review

Editorial Board Memberships

Program Committees

  • LICS 2022 – 37th Annual Symposium on Logic in Computer Science
  • POPL 2022 – 48th ACM SIGPLAN Symposium on Principles of Programming Languages
  • CAV 2021 – 33rd Int’l Conf. on Computer-Aided Verification
  • CONCUR 2020 – 31st Int’l Conf. on Concurrency Theory, part of QONFEST 2020
  • LPAR23 – 23rd Int’l Conf. on Logic for Programming, Artificial Intelligence and Reasoning (2020)
  • QEST 2019 – 16th Int’l Conf. on Quantitative Evaluation of SysTems
  • QEST 2018 – 15th Int’l Conf. on Quantitative Evaluation of SysTems, 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

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

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

I am a founding director of The Weissbord Institute.

2022
DOI fulltext PDF [bibtex]
@article{W2022,
title = {Weighted programming: a programming paradigm for specifying mathematical models},
author = {Kevin Batz and Adrian Gallus and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Tobias Winkler},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
pages = {pages 66},
type = {Journal Article},
year = {2022},
doi = {10.1145/3527310},
url = { https://publications.rwth-aachen.de/record/845157},
}×
[issue] 		Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler. Weighted programming: a programming paradigm for specifying mathematical models, Proceedings of the ACM on programming languages, pages 66, ACM, 2022.
2021
DOI [bibtex]
@conference{GFPP2021,
title = {Generating Functions for Probabilistic Programs},
author = {Lutz Klinkenberg and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Joshua Moerman and Tobias Winkler},
publisher = {Springer},
booktitle = {Theoretical Computer Science and General Issues},
volume = {12561},
pages = {231-248},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-68446-4_12},
url = { https://publications.rwth-aachen.de/record/807881},
}×
[issue] 		Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. Generating Functions for Probabilistic Programs, 30. International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2020), Volume 12561 of Theoretical Computer Science and General Issues, 231-248, Springer, 2021.
2020
DOI [bibtex]
@article{A2020,
title = {Aiming low is harder: induction for lower bounds in probabilistic program verification},
author = {Marcel Tobias Hark and Benjamin Lucien Kaminski and Jürgen Giesl and Joost-Pieter Katoen},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {4(POPL)},
pages = {pages 1-28},
type = {Journal Article},
year = {2020},
doi = {10.1145/3371105},
url = { https://publications.rwth-aachen.de/record/784743},
}×
[issue] 		Marcel Tobias Hark, Benjamin Lucien Kaminski, Jürgen Giesl, Joost-Pieter Katoen. Aiming low is harder: induction for lower bounds in probabilistic program verification, Proceedings of the ACM on programming languages 4 (POPL), pages 1-28, ACM, 2020.
arXiv:2004.14835 [bibtex]
@unpublished{PPDRM2020,
title = {PrIC3: Property Directed Reachability for MDPs},
author = {Kevin Batz and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schroer},
type = {Preprint},
year = {2020},
url = { https://arxiv.org/abs/2004.14835},
}×
[issue] 		Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schroer. PrIC3: Property Directed Reachability for MDPs, 2020. https://arxiv.org/abs/2004.14835
DOI [bibtex]
@conference{GDCD2020,
title = {Generative Datalog with Continuous Distributions},
author = {Martin Grohe and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Peter Lindner},
publisher = {ACM},
pages = {347-360},
type = {Conference Paper},
year = {2020},
doi = {10.1145/3375395.3387659},
url = { https://publications.rwth-aachen.de/record/794402},
}×
[issue] 		Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Peter Lindner. Generative Datalog with Continuous Distributions, 39. ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2020), 347-360, ACM, 2020.
arXiv:2007.06327 [bibtex]
@unpublished{GFPP2020,
title = {Generating Functions for Probabilistic Programs},
author = {Lutz Klinkenberg and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Joshua Moerman and Tobias Winkler},
type = {Preprint},
year = {2020},
url = { https://arxiv.org/abs/2007.06327},
}×
[issue] 		Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. Generating Functions for Probabilistic Programs, 2020. https://arxiv.org/abs/2007.06327
fulltext PDF [bibtex]
@techreport{URTGURAVL2020,
title = {UnRAVeL Research Training Group: Uncertainty and Randomness in Algorithms, Verification, and Logic},
author = {Joost-Pieter Katoen and Martin Ritzert and Richard Marlon Wilke and Katrin M. Dannert and Peter Lindner and Dennis Fischer and Janosch Fuchs and Björn Frederik Tauer and Vipin Ravindran Vijayalakshmi and Laura Vargas Koch and Nadine Friesen and Andreas Gabriel Klinger and Marcel Tobias Hark and Benjamin Lucien Kaminski and Sebastian Junges and Jip Josephine Spel and Anton Pirogov and Stefan Schupp and Till Hofmann and Daxin Liu and Martin Comis and Tabea Claudia Krabs and Stephan Zieger and Rebecca Haehn and Matthias Volk and Norman Weik and Helene-Maria Bolke-Hermanns},
pages = {85 Seiten},
type = {Tech Report},
year = {2020},
url = { https://publications.rwth-aachen.de/record/807487},
}×
[issue] 		Joost-Pieter Katoen, Martin Ritzert, Richard Marlon Wilke, Katrin M. Dannert, Peter Lindner, Dennis Fischer, Janosch Fuchs, Björn Frederik Tauer, Vipin Ravindran Vijayalakshmi, Laura Vargas Koch, Nadine Friesen, Andreas Gabriel Klinger, Marcel Tobias Hark, Benjamin Lucien Kaminski, Sebastian Junges, Jip Josephine Spel, Anton Pirogov, Stefan Schupp, Till Hofmann, Daxin Liu, Martin Comis, Tabea Claudia Krabs, Stephan Zieger, Rebecca Haehn, Matthias Volk, Norman Weik, Helene-Maria Bolke-Hermanns. UnRAVeL Research Training Group: Uncertainty and Randomness in Algorithms, Verification, and Logic, 85 Seiten, 2020.
DOI fulltext PDF [bibtex]
@conference{PPDRM2020,
title = {PrIC3: Property Directed Reachability for MDPs},
author = {Kevin Batz and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
publisher = {Springer},
booktitle = {LNCS},
volume = {12225},
pages = {512-538},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-53291-8_27},
url = { https://publications.rwth-aachen.de/record/816242},
}×
[issue] 		Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. PrIC3: Property Directed Reachability for MDPs, 32. International Conference on Computer Aided Verification (CAV 2020), Volume 12225 of LNCS, 512-538, Springer, 2020.
fulltext PDF [bibtex]
@conference{VPP2020,
title = {Verifying Probabilistic Programs},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {12289},
pages = {298-298},
type = {Conference Paper},
year = {2020},
url = { https://publications.rwth-aachen.de/record/834060},
}×
[issue] 		Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Verifying Probabilistic Programs, 17. International Conference on Quantitative Evaluation of SysTems (QEST 2020), Volume 12289 of LNCS, 298-298, Springer, 2020.
2019
DOI [bibtex]
@article{O2019,
title = {On the hardness of analyzing probabilistic programs},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
journal = {Acta informatica},
volume = {56(3)},
pages = {pages 255-285},
type = {Journal Article},
year = {2019},
doi = {10.1007/s00236-018-0321-1},
url = { https://publications.rwth-aachen.de/record/753077},
}×
[issue] 		Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the hardness of analyzing probabilistic programs, Acta informatica 56 (3), pages 255-285, Springer, 2019.
DOI fulltext PDF [bibtex]
@article{Q2019,
title = {Quantitative separation logic: a logic for reasoning about probabilistic pointer programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {3(POPL)},
pages = {pages 34},
type = {Journal Article},
year = {2019},
doi = {10.1145/3290347},
url = { https://publications.rwth-aachen.de/record/753722},
}×
[issue] 		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, ACM, 2019.
DOI fulltext PDF [bibtex]
@phdthesis{A2019,
title = {Advanced weakest precondition calculi for probabilistic programs},
author = {Benjamin Lucien Kaminski},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (xiv, 363 Seiten) : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2019},
doi = {10.18154/RWTH-2019-01829},
url = { https://publications.rwth-aachen.de/record/755408},
}×
[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.
2018
DOI [bibtex]
@article{CPP2018,
title = {Conditioning in Probabilistic Programming},
author = {Federico Olmedo and Friedrich Gretz and Nils Jansen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Annabelle Mciver},
publisher = {Association for Computing Machinery},
journal = {ACM transactions on programming languages and systems},
volume = {40(1)},
pages = {pages 4},
type = {Journal Article},
year = {2018},
doi = {10.1145/3156018},
url = { https://publications.rwth-aachen.de/record/713137},
}×
[issue] 		Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle Mciver. Conditioning in Probabilistic Programming, ACM transactions on programming languages and systems 40 (1), pages 4, Association for Computing Machinery, 2018.
DOI [bibtex]
@article{A2018,
title = {A new proof rule for almost-sure termination},
author = {Annabelle McIver and Carroll Morgan and Benjamin Lucien Kaminski and Joost-Pieter Katoen},
publisher = {ACM},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
pages = {pages 33:1-33:28},
type = {Journal Article},
year = {2018},
doi = {10.1145/3158121},
url = { https://publications.rwth-aachen.de/record/753060},
}×
[issue] 		Annabelle McIver, Carroll Morgan, 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, ACM, 2018.
DOI fulltext PDF [bibtex]
@conference{HOBIA2018,
title = {How long, O Bayesian network, will I sample thee?: A program analysis perspective on expected sampling times},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {10801},
pages = {186-213},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-89884-1_7},
url = { https://publications.rwth-aachen.de/record/753062},
}×
[issue] 		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, 27. European Symposium on Programming (ESOP 2018), Volume 10801 of LNCS, 186-213, Springer, 2018.
arXiv:1802.10467 [bibtex]
@unpublished{QSLALRPP2018,
title = {Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
pages = {159 Seiten},
type = {Preprint},
year = {2018},
url = { https://arxiv.org/abs/1802.10467},
}×
[issue] 		Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Programs, 159 Seiten, 2018. https://arxiv.org/abs/1802.10467
DOI [bibtex]
@article{WPRERRA2018,
title = {Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Federico Olmedo},
journal = {Journal of the ACM},
volume = {65(5)},
pages = {pages 30:1-30:68},
type = {Journal Article},
year = {2018},
doi = {10.1145/3208102},
url = { https://publications.rwth-aachen.de/record/753072},
}×
[issue] 		Benjamin 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.
DOI [bibtex]
@conference{RBCPD2018,
title = {Rule-Based Conditioning of Probabilistic Data},
author = {Maurice van Keulen and Benjamin Lucien Kaminski and Christoph Matheja and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {Lecture Notes in Artificial Intelligence},
volume = {11142},
pages = {290-305},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-030-00461-3_20},
url = { https://publications.rwth-aachen.de/record/753086},
}×
[issue] 		Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. Rule-Based Conditioning of Probabilistic Data, 12. International Conference on Scalable Uncertainty Management (SUM 2018), Volume 11142 of Lecture Notes in Artificial Intelligence, 290-305, Springer, 2018.
2017
DOI [bibtex]
@conference{AWPESMSE2017,
title = {A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen},
publisher = {IEEE},
pages = {1-12},
type = {Conference Paper},
year = {2017},
doi = {10.1109/LICS.2017.8005153},
url = { https://publications.rwth-aachen.de/record/713562},
}×
[issue] 		Benjamin Lucien Kaminski, Joost-Pieter Katoen. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations, 32. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), 1-12, IEEE, 2017.
2016
DOI [bibtex]
@conference{RRPP2016,
title = {Reasoning about Recursive Probabilistic Programs},
author = {Federico Olmedo Beron and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {ACM Press},
pages = {672-681},
type = {Conference Paper},
year = {2016},
doi = {10.1145/2933575.2935317},
url = { https://publications.rwth-aachen.de/record/680115},
}×
[issue] 		Federico Olmedo Beron, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Reasoning about Recursive Probabilistic Programs, 31. Annual ACM/IEEE Symposium, 672-681, ACM Press, 2016.
DOI [bibtex]
@conference{ICPP2016,
title = {Inferring Covariances for Probabilistic Programs},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {9826},
pages = {191-206},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-43425-4_14},
url = { https://publications.rwth-aachen.de/record/680858},
}×
[issue] 		Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Inferring Covariances for Probabilistic Programs, 13. International Conference on Quantitative Evaluation of Systems (QEST 2016), Volume 9826 of LNCS, 191-206, Springer, 2016.
DOI [bibtex]
@conference{BMCPP2016,
title = {Bounded Model Checking for Probabilistic Programs},
author = {Nils Jansen and Hans Christian Dehnert and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Lukas Westhofen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9938},
pages = {68-85},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-46520-3_5},
url = { https://publications.rwth-aachen.de/record/681511},
}×
[issue] 		Nils Jansen, Hans Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen. Bounded Model Checking for Probabilistic Programs, 14. International Symposium on Automated Technology for Verification and Analysis (ATVA), Volume 9938 of LNCS, 68-85, Springer, 2016.
fulltext PDF [bibtex]
@misc{OSIC2016,
title = {On the Semantic Intricacies of Conditioning},
author = {Friedrich Gretz and Nils Jansen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Federico Olmedo Beron},
pages = {2 Seiten},
type = {Invited Abstract},
year = {2016},
url = { https://publications.rwth-aachen.de/record/684633},
}×
[issue] 		Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo Beron. On the Semantic Intricacies of Conditioning, 2 Seiten, 2016.
DOI [bibtex]
@conference{WPRERTPP2016,
title = {Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Federico Olmedo Beron},
publisher = {Springer},
booktitle = {LNCS},
volume = {9632},
pages = {364-389},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-662-49498-1_15},
url = { https://publications.rwth-aachen.de/record/684643},
}×
[issue] 		Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo Beron. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs, 25. European Symposium on Programming (ESOP 2016), Volume 9632 of LNCS, 364-389, Springer, 2016.
2015
DOI fulltext PDF [bibtex]
@article{CPP2015,
title = {Conditioning in Probabilistic Programming},
author = {Nils Jansen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Federico Olmedo and Friedrich Gretz and Annabelle McIver},
publisher = {Elsevier Science},
journal = {Electronic notes in theoretical computer science},
volume = {319},
pages = {pages 199-216},
type = {Journal Article},
year = {2015},
doi = {10.1016/j.entcs.2015.12.013},
url = { https://publications.rwth-aachen.de/record/571612},
}×
[issue] 		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, Elsevier Science, 2015.
DOI [bibtex]
@conference{OHAST2015,
title = {On the Hardness of Almost–Sure Termination},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9234},
pages = {308-318},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-662-48057-1_24},
url = { https://publications.rwth-aachen.de/record/571614},
}×
[issue] 		Benjamin Lucien Kaminski, Joost-Pieter Katoen. On the Hardness of Almost–Sure Termination, 40. International Symposium on Mathematical Foundations of Computer Science (MFCS 2015), Volume 9234 of LNCS, 308-318, Springer, 2015.
DOI [bibtex]
@conference{UPP2015,
title = {Understanding Probabilistic Programs},
author = {Joost-Pieter Katoen and Friedrich Gretz and Nils Jansen and Benjamin Lucien Kaminski and Federico Olmedo Beron},
publisher = {Springer},
booktitle = {LNCS},
volume = {9360},
pages = {15-32},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-23506-6_4},
url = { https://publications.rwth-aachen.de/record/571617},
}×
[issue] 		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 60. Birthday, Volume 9360 of LNCS, 15-32, Springer, 2015.
[bibtex]
@conference{PPANMAC2015,
title = {Probabilistic Programs - A Natural Model for Approximate Computations},
author = {Nils Jansen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Federico Olmedo},
type = {Conference Paper},
year = {2015},
url = { https://publications.rwth-aachen.de/record/571634},
}×
[issue] 		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.