Caesar: A Verifier for Probabilistic Programs

on YouTube ↗18m

" summary

A deductive verifier called Caesar implements a probabilistic Boogie‑style pipeline: programs, specifications and proof rules are encoded in the quantitative IVL Havier, a weakest‑pre‑expectation VC generator emits formulas in the real‑valued logic Halo, and an SMT‑backed Rust toolserver tries to discharge them. The published OOPSLA ’23 infrastructure automatically verifies 40+ benchmarks, supports lower/upper bounds, almost‑sure and positive almost‑sure termination, 12 loop proof rules, recursion and user data, and is available at caesarverify.org.

AI-written summary · about

" chapters (11)

1. 0:00Caesar verifier intro
2. 1:56Probabilistic program properties
3. 3:20Caesar design goals
4. 5:30Weakest pre-expectations in Haviar
5. 8:21GD implication semantics
6. 9:05Probabilistic loop example
7. 11:13Upper bound reasoning in Haviar
8. 12:38Proof rules and case studies
9. 13:40Loop invariance rule
10. 15:07Caesar tool details
11. 15:51Q&A