Automated Safety Verification of Posterior Distributions of Probabilistic Programs

Abstract

Ensuring the safety of probabilistic systems is a central challenge in formal verification. We propose an automated refinement technique for verifying a safety property of posterior distributions in probabilistic programs. Our approach builds on the counterexample-guided abstraction refinement (CEGAR) framework and exploits the duality in convex optimisation and the adequacy of predicate-transformer semantics in probabilistic settings. We implement the technique and evaluate its effectiveness through preliminary experiments.