Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back

Kevin Batz, Joost-Pieter Katoen, Francesca Randone +1

We lay out novel foundations for the computer-aided verification of guaranteed bounds on expected outcomes of imperative probabilistic programs featuring (i) general loops, (ii) co…