activity
20142026
most citedAiming Low Is Harder -- Induction for Lower Bounds in Probabilistic Program Verification

47 citations · 183 across the 23 of their papers we have counts for

collaborators
Showing 2024Show all

2 papers · 1 filter

cs.LO2024★ 2 cited

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

Markov decision processes (MDPs) with rewards are a widespread and well-studied model for systems that make both probabilistic and nondeterministic choices. A fundamental result ab…

cs.LO2024

Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers

Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski +1

We present a novel \emph{weakest pre calculus} for \emph{reasoning about quantitative hyperproperties} over \emph{nondeterministic and probabilistic} programs. Whereas existing cal…