Automated deductive verification of probabilistic programs

Batz, Kevin; Hasuo, Ichiro; Katoen, Joost-Pieter

doi:10.18154/RWTH-2025-00473

Automated deductive verification of probabilistic programs

Batz, Kevin^RWTH*

2024 & 2025

Verantwortlichkeitsangabevorgelegt von Kevin Stefan Batz, M. Sc.

ImpressumAachen : RWTH Aachen University 2024

Umfang1 Online-Ressource : Illustrationen

Dissertation, RWTH Aachen University, 2024

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2025

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Hasuo, Ichiro (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2024-12-20

Online
DOI: 10.18154/RWTH-2025-00473
URL: http://publications.rwth-aachen.de/record/1002329/files/1002329.pdf

Einrichtungen

Projekte

FRAPPANT - Formal Reasoning About Probabilistic Programs: Breaking New Ground for Automation (787914) (787914)

Inhaltliche Beschreibung (Schlagwörter)
Markov decision processes (frei) ; fixed point theory (frei) ; formal verification (frei) ; invariant synthesis (frei) ; probabilistic model checking (frei) ; probabilistic programs (frei) ; quantitative verification (frei) ; weakest preexpectation (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Wir studieren sowohl grundlegende als auch praktische Aspekte der automatisierten deduktiven Verifikation von diskreten probabilistischen Programmen. Unser besonderer Schwerpunkt liegt auf der Verifikation von möglicherweise unbeschränkten Schleifen mittels quantitativer Schleifeninvarianten. Wir bauen auf Kozens, McIver & Morgans und Kaminskis Kalkül der Schwächsten Vorerwartung auf, um erwartete Ergebnisse, wie z.B. die Wahrscheinlichkeit, in einer Nachbedingung zu terminieren oder den erwarteten finalen Wert einer Programmvariablen, zu ermitteln. Der Kalkül der Schwächsten Vorerwartung ersetzt Prädikate aus der klassischen Programmverifikation durch allgemeinere Erwartungen --- Funktionen, die Programmzustände auf Zahlen anstelle von Wahrheitswerten abbilden. Wir untersuchen eine Syntax zur Spezifikation von Erwartungen, die eine Grundlage für automatisierte deduktive probabilistische Programmverifizierer liefert. Wir beweisen, dass unsere Syntax aussagekräftig ist und erhalten so ein relativ vollständiges Verifikationssystem für erwartete Ergebnisse. Anschließend stellen wir drei verschiedene Ansätze für die automatisierte Verifikation von Schranken auf erwartete Ergebnisse linearer Schleifen. Diese Ansätze kombinieren den Kalkül der Schwächsten Vorerwartung mit Techniken der Erfüllbarkeit Modulo Theorien:1. Wir betrachten zwei etablierte Verifikationstechniken für Übergangssysteme, k-Induktion und begrenzte Modellüberprüfung (BMÜ), im allgemeineren Rahmen der Begrenzung kleinster Fixpunkte von Funktionen über vollständigen Verbänden. Dies führt zu vergitterter $k$-Induktion und vergitterter BM\"U führt. Die Instanziierung unserer vergitterten Techniken mit dem Kalkül der Schwächsten Vorerwartung ermöglicht die vollautomatische Verifikation von linearen Schleifen, die aus der Literatur stammen. 2. Wir präsentieren einen gegenbeispielgeleiteten induktiven Syntheseansatz für die Synthese quantitativer Schleifeninvarianten. Dies ermöglicht die vollautomatische Verifikation von Schranken auf erwartete Ergebnisse und erwartete Laufzeiten. Unsere Implementierung synthetisiert quantitative Invarianten verschiedener linearer Schleifen aus der Literatur, kann modernste probabilistische Modellprüfer für Programme mit endlichen Zustandsräumen schlagen und ist mit modernen Werkzeugen konkurrenzfähig, die sich der Invariantensynthese oder dem berechnen erwarteter Laufzeiten widmen.3.Wir präsentieren PrIC3 --- die erste wirklich quantitative Erweiterung des modernen qualitativen symbolischen Modellprüfungsalgorithmus IC3 zur symbolischen Modellprüfung von Markov-Entscheidungsprozessen. Durch das Verbinden von PrIC3 mit dem Kalkül der Schwächsten Vorerwartung erhalten wir einen symbolischen Modellprüfungsalgorithmus für probabilistische Programme. Wir stellen eine Implementierung von PrIC3 vor, die IC3-spezifische Techniken, wie z.B. Generalisierung, beinhaltet.

We study both foundational and practical aspects of the automated deductive verification of discrete probabilistic programs. Our special emphasis is on the verification of possibly unbounded loops by quantitative loop invariants. We build upon Kozen's, McIver & Morgan's, and Kaminski's weakest preexpectation calculus for reasoning about expected outcomes such as the probability of terminating in some postcondition or the expected final value of a program variable. The weakest preexpectation calculus replaces predicates from classical program verification by more general expectations --- functions mapping program states to numbers instead of truth values. We study a syntax for specifying expectations, providing a foundation for automated deductive probabilistic program verifiers. We prove that our syntax is expressive and hence obtain a relatively complete verification system for reasoning about expected outcomes. We then present three different approaches for automating the verification of bounds on expected outcomes of linear loops, all of which combine weakest preexpectation reasoning with Satisfiability Modulo Theories (SMT) techniques: 1. We revisit two well-established verification techniques for transition systems, k-induction and bounded model checking (BMC), in the more general setting of bounding least fixpoints of functions over complete lattices, yielding latticed k-induction and latticed BMC. Instantiating our latticed techniques with the weakest preexpectation calculus enables the fully automatic verification of linear loops taken from the literature. 2. We present a counterexample-guided inductive synthesis approach for the synthesis of quantitative loop invariants. This enables the fully automatic verification of bounds on both expected outcomes and expected runtimes. Our implementation synthesizes quantitative invariants of various linear loops taken from the literature, can beat state-of-the-art probabilistic model checkers on finite-state programs, and is competitive with modern tools dedicated to invariant synthesis or expected runtime reasoning. 3. We present PrIC3 --- the first truly quantitative extension of the state-of-the-art qualitative symbolic model checking algorithm IC3 to symbolic model checking of Markov decision processes. By marrying PrIC3 with the weakest preexpectation calculus, we obtain a symbolic model checking algorithm for probabilistic programs. Alongside, we present an implementation of PrIC3 featuring IC3-specific techniques such as generalization.

OpenAccess:
PDF
(additional files)