Caesar: A Verifier for Probabilistic Programs - Dafny'24

Explore a groundbreaking verifier for probabilistic programs in this 18-minute conference talk from ACM SIGPLAN. Delve into Caesar, a novel deductive verification infrastructure first introduced at OOPSLA '2023. Discover the basics of this infrastructure and its implementation, drawing parallels to Boogie as a probabilistic counterpart. Examine the key components, including an intermediate verification language (IVL) and a real-valued logic, designed to handle quantitative properties such as expected outcomes, run-times, and termination probabilities. Learn about the paradigm shift from Boolean to real-valued domains in verification, and understand how the IVL incorporates quantitative generalizations of standard verification constructs. Gain insights into the weakest-precondition-style semantics for generating verification conditions and the SMT-based implementation that enables automatic verification of various benchmarks. Recognize the significance of this infrastructure as the first of its kind for expectation-based reasoning about probabilistic programs.