A deductive verifier for probabilistic programs

Schroer, Philipp; Matheja, Christoph; Batz, Kevin; Müller, Peter; Kaminski, Benjamin; Katoen, Joost-Pieter

doi:10.18154/RWTH-2024-11340

A deductive verifier for probabilistic programs

Schroer, Philipp^RWTH*

2024

Verantwortlichkeitsangabeby Philipp Schroer

ImpressumAachen : RWTH Aachen University 2024

Umfang1 Online-Ressource: Illustrationen

Masterarbeit, RWTH Aachen University, 2022

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2024

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Müller, Peter (Thesis advisor) ; Batz, Kevin (Consultant)^RWTH* ; Kaminski, Benjamin (Consultant)^RWTH* ; Matheja, Christoph (Consultant)^RWTH*

Tag der mündlichen Prüfung/Habilitation
2022-01-25

Online
DOI: 10.18154/RWTH-2024-11340
URL: https://publications.rwth-aachen.de/record/998370/files/998370.pdf

Einrichtungen

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
We design and implement a deductive verification infrastructure for probabilistic programs. It consists of a quantitative intermediate verification language (HeyVL) and a quantitative assertion language (HeyLo). HeyLo is a syntax to express expected values of probabilistic programs, with support for quantitative implications based on Gödel logic. Both HeyLo and HeyVL contain lattice-theoretic dual constructs to reason about lower and upper bounds of expected values. As a case study, we encode weakest pre-expectation and weakest liberal pre-expectation reasoning about the probabilistic programming language pGCL into HeyVL. For loops, we provide encodings of Park induction, k-induction, and bounded model checking. Park induction and k-induction are both proof rules that require on user-provided invariant candidates. Furthermore, we discuss the automation of our deductive verification infrastructure. Our implementation Caesar takes a HeyVL program as input, generates and optimizes verification conditions in the form of HeyLo formulas and uses the automated theorem prover Z3 to prove or disprove validity of the verification conditions. In this thesis, we focus on the central optimization of quantifier elimination of HeyLo formulas. We present early promising experimental results. Finally, we discuss the abstraction of our framework based on Heyting and Gödel algebras to support more domains than expectations.

OpenAccess:
PDF