Benjamin Lucien Kaminski

79 papers A* 3A 3B 2C 1Journal 53Unranked 11
YearRankTypeTitle / Venue / Authors
2026 J jnl
Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops (Extended Version).
CoRR
Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler
2026 — conf
Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops.
ESOP (1)
Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler
2026 J jnl
noDice: Inference for Discrete Probabilistic Programs with Nondeterminism and Conditioning.
CoRR
Tobias Gürtler, Benjamin Lucien Kaminski
2025 J jnl
A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests.
Proc. ACM Program. Lang.
Lena Verscht, Benjamin Lucien Kaminski
2025 J jnl
Partial Incorrectness Logic.
CoRR
Lena Verscht, Anrán Wáng, Benjamin Lucien Kaminski
2025 — conf
Programming and Reasoning in Partially Observable Probabilistic Environments.
QEST+FORMATS
Tobias Gürtler, Benjamin Lucien Kaminski
2025 J jnl
Programming and Reasoning in Partially Observable Probabilistic Environments.
CoRR
Tobias Gürtler, Benjamin Lucien Kaminski
2025 J jnl
Replicable theory.
Int. J. Softw. Tools Technol. Transf.
Benjamin Lucien Kaminski
2024 J jnl
A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests.
CoRR
Lena Verscht, Benjamin Lucien Kaminski
2024 — conf
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.
Principles of Verification (1)
Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja, Tobias Winkler
2024 J jnl
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).
CoRR
Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja, Tobias Winkler
2024 — ed.
Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part I
Principles of Verification (1)
Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk
2024 — ed.
Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part II
Principles of Verification (2)
Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk
2024 — ed.
Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III
Principles of Verification (3)
Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk
2024 J jnl
Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers.
CoRR
Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski, Alexandra Silva
2024 J jnl
Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers.
Proc. ACM Program. Lang.
Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski, Alexandra Silva
2023 J jnl
A Calculus for Amortized Expected Runtimes.
Proc. ACM Program. Lang.
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht
2023 J jnl
A Deductive Verification Infrastructure for Probabilistic Programs.
CoRR
Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2023 J jnl
A Deductive Verification Infrastructure for Probabilistic Programs.
Proc. ACM Program. Lang.
Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2023 J jnl
Hoare-Like Triples and Kleene Algebras with Top and Tests: Towards a Holistic Perspective on Hoare Logic, Incorrectness Logic, and Beyond.
CoRR
Lena Verscht, Benjamin Lucien Kaminski
2023 J jnl
Lower Bounds for Possibly Divergent Probabilistic Programs.
CoRR
Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan
2023 J jnl
Lower Bounds for Possibly Divergent Probabilistic Programs.
Proc. ACM Program. Lang.
Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan
2023 — conf
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants.
TACAS (2)
Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2023 J jnl
The 19th International Workshop on Termination (WST 2023): Preface, Invited Talk Abstract, and Tool Descriptions.
CoRR
Akihisa Yamada, Benjamin Lucien Kaminski, Dieter Hofbauer, Fred Mesnard, Étienne Payet
2022 J jnl
A Calculus for Amortized Expected Runtimes.
CoRR
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht
2022 J jnl
Generative Datalog with Continuous Distributions.
J. ACM
Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Peter Lindner
2022 J jnl
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants.
CoRR
Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2022 J jnl
Quantitative Strongest Post.
CoRR
Linpeng Zhang, Benjamin Lucien Kaminski
2022 J jnl
Quantitative strongest post: a calculus for reasoning about the flow of quantitative information.
Proc. ACM Program. Lang.
Linpeng Zhang, Benjamin Lucien Kaminski
2022 J jnl
Weighted Programming.
CoRR
Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler
2022 J jnl
Weighted programming: a programming paradigm for specifying mathematical models.
Proc. ACM Program. Lang.
Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler
2021 J jnl
A pre-expectation calculus for probabilistic sensitivity.
Proc. ACM Program. Lang.
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2021 — conf
Latticed k-Induction with an Application to Probabilistic Programs.
CAV (2)
Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
2021 J jnl
Latticed k-Induction with an Application to Probabilistic Programs.
CoRR
Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
2021 J jnl
Probabilistic Data with Continuous Distributions.
CoRR
Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Peter Lindner
2021 J jnl
Probabilistic Data with Continuous Distributions.
SIGMOD Rec.
Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Peter Lindner
2021 J jnl
Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning.
Proc. ACM Program. Lang.
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2020 J jnl
Aiming low is harder: induction for lower bounds in probabilistic program verification.
Proc. ACM Program. Lang.
Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, Joost-Pieter Katoen
2020 — ch.
Expected Runtime Analyis by Program Verification.
Foundations of Probabilistic Programming
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2020 C conf
Generating Functions for Probabilistic Programs.
LOPSTR
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler
2020 J jnl
Generating Functions for Probabilistic Programs.
CoRR
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler
2020 A* conf
Generative Datalog with Continuous Distributions.
PODS
Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Peter Lindner
2020 J jnl
Generative Datalog with Continuous Distributions.
CoRR
Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Peter Lindner
2020 — conf
Optimistic Value Iteration.
CAV (2)
Arnd Hartmanns, Benjamin Lucien Kaminski
2020 — conf
PrIC3: Property Directed Reachability for MDPs.
CAV (2)
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
2020 J jnl
PrIC3: Property Directed Reachability for MDPs.
CoRR
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
2020 J jnl
Relatively Complete Verification of Probabilistic Programs.
CoRR
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2019 — —
Advanced weakest precondition calculi for probabilistic programs.
Benjamin Lucien Kaminski
2019 J jnl
Aiming Low Is Harder - Inductive Proof Rules for Lower Bounds on Weakest Preexpectations in Probabilistic Program Verification.
CoRR
Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, Joost-Pieter Katoen
2019 — ch.
Erweiterte Verifikationskalküle für Probabilistische Programme.
Ausgezeichnete Informatikdissertationen
Benjamin Lucien Kaminski
2019 J jnl
Kantorovich Continuity of Probabilistic Programs.
CoRR
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2019 J jnl
On the hardness of analyzing probabilistic programs.
Acta Informatica
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2019 J jnl
Optimistic Value Iteration.
CoRR
Arnd Hartmanns, Benjamin Lucien Kaminski
2019 J jnl
Quantitative separation logic: a logic for reasoning about probabilistic pointer programs.
Proc. ACM Program. Lang.
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll
2018 J jnl
A new proof rule for almost-sure termination.
Proc. ACM Program. Lang.
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen
2018 J jnl
Conditioning in Probabilistic Programming.
ACM Trans. Program. Lang. Syst.
Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver
2018 A conf
How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times.
ESOP
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2018 J jnl
How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times.
CoRR
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2018 J jnl
Quantitative Separation Logic.
CoRR
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll
2018 — conf
Rule-Based Conditioning of Probabilistic Data.
SUM
Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen
2018 J jnl
Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms.
J. ACM
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo
2017 J jnl
A New Proof Rule for Almost-Sure Termination.
CoRR
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen
2017 J jnl
A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations.
CoRR
Benjamin Lucien Kaminski, Joost-Pieter Katoen
2017 A* conf
A weakest pre-expectation semantics for mixed-sign expectations.
LICS
Benjamin Lucien Kaminski, Joost-Pieter Katoen
2016 B conf
Bounded Model Checking for Probabilistic Programs.
ATVA
Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen
2016 J jnl
Bounded Model Checking for Probabilistic Programs.
CoRR
Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen
2016 — conf
Inferring Covariances for Probabilistic Programs.
QEST
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2016 J jnl
Inferring Covariances for Probabilistic Programs.
CoRR
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2016 A* conf
Reasoning about Recursive Probabilistic Programs.
LICS
Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2016 J jnl
Reasoning about Recursive Probabilistic Programs.
CoRR
Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2016 A conf
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs.
ESOP
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo
2016 J jnl
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs.
CoRR
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo
2015 J jnl
Conditioning in Probabilistic Programming.
CoRR
Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver, Federico Olmedo
2015 B conf
Conditioning in Probabilistic Programming.
MFPS
Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo, Friedrich Gretz, Annabelle McIver
2015 — conf
On the Hardness of Almost-Sure Termination.
MFCS (1)
Benjamin Lucien Kaminski, Joost-Pieter Katoen
2015 J jnl
On the Hardness of Almost-Sure Termination.
CoRR
Benjamin Lucien Kaminski, Joost-Pieter Katoen
2015 — conf
Understanding Probabilistic Programs.
Correct System Design
Joost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Federico Olmedo
2014 J jnl
Analyzing Expected Outcomes and Almost-Sure Termination of Probabilistic Programs is Hard.
CoRR
Benjamin Lucien Kaminski, Joost-Pieter Katoen
2011 A conf
Scalable Symbolic Execution of Distributed Systems.
ICDCS
Raimondas Sasnauskas, Oscar Soria Dustmann, Benjamin Lucien Kaminski, Klaus Wehrle, Carsten Weise, Stefan Kowalewski