---
title: "Automated Safety Verification of Posterior Distributions of Probabilistic Programs"
authors:
  - "Kazuki Watanabe"
  - "Hiroshi Unno"
doi: "10.24963/ijcai.2026/91"
url: "https://ijcai.org/proceedings/2026/91"
pdf: "https://ijcai.org/proceedings/2026/0091.pdf"
venue: "Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence"
year: 2026
pages: "807-816"
track: "Main Track"
keywords:
  - "Constraint Satisfaction and Optimization: Constraint satisfaction"
  - "AI Ethics, Trust, Fairnes: Safety and robustness"
  - "Knowledge Representation and Reasoning: Automated reasoning and theorem proving"
  - "Constraint Satisfaction and Optimization: Solvers and tools"
  - "Constraint Satisfaction and Optimization: Satisfiabilty"
---

# Automated Safety Verification of Posterior Distributions of Probabilistic Programs

Kazuki Watanabe, Hiroshi Unno

*Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence*, pages 807-816. DOI: [10.24963/ijcai.2026/91](https://doi.org/10.24963/ijcai.2026/91)

## 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.