A Deductive Verification Infrastructure for Probabilistic Programs

Explore a groundbreaking deductive verification infrastructure for discrete probabilistic programs in this 17-minute conference talk from OOPSLA2 2023. Delve into the development of a quantitative program verification system, analogous to Boogie, featuring an intermediate verification language (IVL) and real-valued logic. Discover how this infrastructure enables verification of quantitative properties such as expected outcomes, run-times, and termination probabilities. Learn about the paradigm shift from Boolean to real-valued domain and the implementation of quantitative generalizations of standard verification constructs. Examine the weakest-precondition-style semantics used for generating verification conditions and understand how this system supports various verification techniques from existing literature. Gain insights into the SMT-based implementation and its application in automatically verifying diverse benchmarks, marking a significant advancement in expectation-based reasoning for probabilistic programs.