Kazuki Watanabe

Automated Safety Verification of Posterior Distributions of Probabilistic Programs

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 (CEGA