Relatively Complete Verification of Probabilistic Programs
summary
Defines a compact grammar for non‑negative real‑valued assertions (rationals, addition, multiplication, truncated subtraction, guarded expectations, scaling and sup/inf quantifiers) and proves closure under weakest pre‑expectation with an effective construction from postexpectation to preexpectation by induction on program structure; loops require encoding rational state sequences and variable-length sums/products (e.g. harmonic numbers, square roots, irrational termination probabilities) syntactically. Result yields constructive wp synthesis and relative completeness up to a single oracle call to decide a syntactic inequality.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:20Non probabilistic programs
- 4:36Syntax
- 6:02Overview
- 6:51Expectations
- 7:52Weakest Pre Expectations
- 9:31Weakest Pre Expectations Examples
- 10:56Weakest Pre Expectations Syntax
- 11:19Prerequisites
- 13:20Arithmetic Expressions
- 14:26Syntax for Expectations
- 19:55Compound Statements
- 24:24Recap
- 25:31Syntax in Action
- 27:37Conclusion
related talks
49mSemantic Foundations for Probabilistic Programming
24mAn Intrinsically-typed Probabilistic Programming Language in Coq (Extended Abstr...
20mVerified Density Compilation for a Probabilistic Programming Language
19mAutomated Verification of Fundamental Algebraic Laws
29mQuantitative strongest post: a calculus for reasoning about the flow of quantitative inform
17mDenotation-based Compositional Compiler Verification
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
19mSimplifying Safety Proofs with Forward-Backward Reasoning and Prophecy