Scalable Symbolic Execution of Distributed Systems. - Raimondas Sasnauskas; Oscar Soria Dustmann; Benjamin Lucien Kaminski; Klaus Wehrle; Carsten Weise; Stefan Kowalewski (ICDCS, 2011)

Analyzing Expected Outcomes and Almost-Sure Termination of Probabilistic Programs is Hard. - Benjamin Lucien Kaminski; Joost-Pieter Katoen (CoRR, 2014)

Understanding Probabilistic Programs. - Joost-Pieter Katoen; Friedrich Gretz; Nils Jansen 001; Benjamin Lucien Kaminski; Federico Olmedo (Correct System Design, 2015)

On the Hardness of Almost-Sure Termination. - Benjamin Lucien Kaminski; Joost-Pieter Katoen (MFCS (1), 2015)

Conditioning in Probabilistic Programming. - Nils Jansen 001; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Federico Olmedo; Friedrich Gretz; Annabelle McIver (MFPS, 2015)

Bounded Model Checking for Probabilistic Programs. - Nils Jansen 001; Christian Dehnert; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Lukas Westhofen 001 (ATVA, 2016)

Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. - Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Federico Olmedo (ESOP, 2016)

Reasoning about Recursive Probabilistic Programs. - Federico Olmedo; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (LICS, 2016)

Inferring Covariances for Probabilistic Programs. - Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (QEST, 2016)

A weakest pre-expectation semantics for mixed-sign expectations. - Benjamin Lucien Kaminski; Joost-Pieter Katoen (LICS, 2017)

How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times. - Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (ESOP, 2018)

Rule-Based Conditioning of Probabilistic Data. - Maurice van Keulen; Benjamin Lucien Kaminski; Christoph Matheja; Joost-Pieter Katoen (SUM, 2018)

Quantitative Separation Logic. - Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Thomas Noll 001 (CoRR, 2018)

Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. - Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Federico Olmedo (J. ACM, 2018)

A new proof rule for almost-sure termination. - Annabelle McIver; Carroll Morgan; Benjamin Lucien Kaminski; Joost-Pieter Katoen (Proc. ACM Program. Lang., 2018)

On the hardness of analyzing probabilistic programs. - Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Acta Informatica, 2019)

Kantorovich Continuity of Probabilistic Programs. - Alejandro Aguirre 001; Gilles Barthe; Justin Hsu; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (CoRR, 2019)

Aiming Low Is Harder - Inductive Proof Rules for Lower Bounds on Weakest Preexpectations in Probabilistic Program Verification. - Marcel Hark; Benjamin Lucien Kaminski; Jürgen Giesl; Joost-Pieter Katoen (CoRR, 2019)

Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. - Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Thomas Noll 001 (Proc. ACM Program. Lang., 2019)

Advanced weakest precondition calculi for probabilistic programs. - Benjamin Lucien Kaminski (2019)

Erweiterte Verifikationskalküle für Probabilistische Programme. - Benjamin Lucien Kaminski (Ausgezeichnete Informatikdissertationen, 2019)

Expected Runtime Analyis by Program Verification. - Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Foundations of Probabilistic Programming, 2020)

PrIC3: Property Directed Reachability for MDPs. - Kevin Batz; Sebastian Junges; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Philipp Schröer (CAV (2), 2020)

Optimistic Value Iteration. - Arnd Hartmanns; Benjamin Lucien Kaminski (CAV (2), 2020)

Generating Functions for Probabilistic Programs. - Lutz Klinkenberg; Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Joshua Moerman; Tobias Winkler 001 (LOPSTR, 2020)

Relatively Complete Verification of Probabilistic Programs. - Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (CoRR, 2020)

Aiming low is harder: induction for lower bounds in probabilistic program verification. - Marcel Hark; Benjamin Lucien Kaminski; Jürgen Giesl; Joost-Pieter Katoen (Proc. ACM Program. Lang., 2020)

Latticed k-Induction with an Application to Probabilistic Programs. - Kevin Batz; Mingshuai Chen; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Philipp Schröer (CAV (2), 2021)

A pre-expectation calculus for probabilistic sensitivity. - Alejandro Aguirre 001; Gilles Barthe; Justin Hsu; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Proc. ACM Program. Lang., 2021)

Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. - Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Proc. ACM Program. Lang., 2021)

Probabilistic Data with Continuous Distributions. - Martin Grohe; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Peter Lindner 001 (SIGMOD Rec., 2021)

Quantitative Strongest Post. - Linpeng Zhang; Benjamin Lucien Kaminski (CoRR, 2022)

Weighted Programming. - Kevin Batz; Adrian Gallus; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Tobias Winkler 001 (CoRR, 2022)

Generative Datalog with Continuous Distributions. - Martin Grohe; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Peter Lindner 001 (J. ACM, 2022)

Weighted programming: a programming paradigm for specifying mathematical models. - Kevin Batz; Adrian Gallus; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Tobias Winkler 001 (Proc. ACM Program. Lang., 2022)

Quantitative strongest post: a calculus for reasoning about the flow of quantitative information. - Linpeng Zhang; Benjamin Lucien Kaminski (Proc. ACM Program. Lang., 2022)

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants. - Kevin Batz; Mingshuai Chen; Sebastian Junges; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (TACAS (2), 2023)

The 19th International Workshop on Termination (WST 2023): Preface, Invited Talk Abstract, and Tool Descriptions. - Akihisa Yamada 002; Benjamin Lucien Kaminski; Dieter Hofbauer; Fred Mesnard; Étienne Payet (CoRR, 2023)

Hoare-Like Triples and Kleene Algebras with Top and Tests: Towards a Holistic Perspective on Hoare Logic, Incorrectness Logic, and Beyond. - Lena Verscht; Benjamin Lucien Kaminski (CoRR, 2023)

A Calculus for Amortized Expected Runtimes. - Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Lena Verscht (Proc. ACM Program. Lang., 2023)

Lower Bounds for Possibly Divergent Probabilistic Programs. - Shenghua Feng; Mingshuai Chen; Han Su 003; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Naijun Zhan (Proc. ACM Program. Lang., 2023)

A Deductive Verification Infrastructure for Probabilistic Programs - Artifact Evaluation. - Philipp Schröer; Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Zenodo, 2023)

A Deductive Verification Infrastructure for Probabilistic Programs. - Philipp Schröer; Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Proc. ACM Program. Lang., 2023)

J-P: MDP. FP. PP - Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs. - Kevin Batz; Benjamin Lucien Kaminski; Christoph Matheja; Tobias Winkler 001 (Principles of Verification (1), 2024)

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report). - Kevin Batz; Benjamin Lucien Kaminski; Christoph Matheja; Tobias Winkler 001 (CoRR, 2024)

Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers. - Linpeng Zhang; Noam Zilberstein; Benjamin Lucien Kaminski; Alexandra Silva 001 (Proc. ACM Program. Lang., 2024)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests. - Lena Verscht; Benjamin Lucien Kaminski (Proc. ACM Program. Lang., 2025)

Partial Incorrectness Logic. - Lena Verscht; Anrán Wáng; Benjamin Lucien Kaminski (CoRR, 2025)

Programming and Reasoning in Partially Observable Probabilistic Environments. - Tobias Gürtler; Benjamin Lucien Kaminski (CoRR, 2025)