A Deductive Verification Infrastructure for Probabilistic Programs

Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

Research output: Contribution to journalJournal articleResearchpeer-review

9 Downloads (Pure)

Abstract

This paper presents a quantitative program verification infrastructure for discrete probabilistic programs. Our infrastructure can be viewed as the probabilistic analogue of Boogie: its central components are an intermediate verification language (IVL) together with a real-valued logic. Our IVL provides a programming-language-style for expressing verification conditions whose validity implies the correctness of a program under investigation. As our focus is on verifying quantitative properties such as bounds on expected outcomes, expected run-times, or termination probabilities, off-the-shelf IVLs based on Boolean first-order logic do not suffice. Instead, a paradigm shift from the standard Boolean to a real-valued domain is required. Our IVL features quantitative generalizations of standard verification constructs such as assume- and assert-statements. Verification conditions are generated by a weakest-precondition-style semantics, based on our real-valued logic. We show that our verification infrastructure supports natural encodings of numerous verification techniques from the literature. With our SMT-based implementation, we automatically verify a variety of benchmarks. To the best of our knowledge, this establishes the first deductive verification infrastructure for expectation-based reasoning about probabilistic programs.
Original languageEnglish
Article number294
JournalProceedings of the ACM on Programming Languages
Volume7
Issue numberOOPSLA2
Number of pages31
ISSN2475-1421
DOIs
Publication statusPublished - 2023

Keywords

  • Deductive verification
  • Quantitative verification
  • Probabilistic programs
  • Weakest preexpectations
  • Real-valued logics
  • Automated reasoning

Fingerprint

Dive into the research topics of 'A Deductive Verification Infrastructure for Probabilistic Programs'. Together they form a unique fingerprint.

Cite this