h1

001002329 001__ 1002329
001002329 005__ 20250213084726.0
001002329 0247_ $$2HBZ$$aHT030935744
001002329 0247_ $$2Laufende Nummer$$a43964
001002329 0247_ $$2datacite_doi$$a10.18154/RWTH-2025-00473
001002329 037__ $$aRWTH-2025-00473
001002329 041__ $$aEnglish
001002329 082__ $$a004
001002329 1001_ $$0P:(DE-82)IDM04047$$aBatz, Kevin$$b0$$urwth
001002329 245__ $$aAutomated deductive verification of probabilistic programs$$cvorgelegt von Kevin Stefan Batz, M. Sc.$$honline
001002329 260__ $$aAachen$$bRWTH Aachen University$$c2024
001002329 260__ $$c2025
001002329 300__ $$a1 Online-Ressource : Illustrationen
001002329 3367_ $$02$$2EndNote$$aThesis
001002329 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
001002329 3367_ $$2BibTeX$$aPHDTHESIS
001002329 3367_ $$2DRIVER$$adoctoralThesis
001002329 3367_ $$2DataCite$$aOutput Types/Dissertation
001002329 3367_ $$2ORCID$$aDISSERTATION
001002329 502__ $$aDissertation, RWTH Aachen University, 2024$$bDissertation$$cRWTH Aachen University$$d2024$$gFak01$$o2024-12-20
001002329 500__ $$aVeröffentlicht auf dem Publikationsserver der RWTH Aachen University 2025
001002329 5203_ $$aWir 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.$$lger
001002329 520__ $$aWe 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.$$leng
001002329 536__ $$0G:(EU-Grant)787914$$aFRAPPANT - Formal Reasoning About Probabilistic Programs: Breaking New Ground for Automation (787914)$$c787914$$fERC-2017-ADG$$x0
001002329 588__ $$aDataset connected to Lobid/HBZ
001002329 591__ $$aGermany
001002329 653_7 $$aMarkov decision processes
001002329 653_7 $$afixed point theory
001002329 653_7 $$aformal verification
001002329 653_7 $$ainvariant synthesis
001002329 653_7 $$aprobabilistic model checking
001002329 653_7 $$aprobabilistic programs
001002329 653_7 $$aquantitative verification
001002329 653_7 $$aweakest preexpectation
001002329 7001_ $$0P:(DE-82)IDM00048$$aKatoen, Joost-Pieter$$b1$$eThesis advisor$$urwth
001002329 7001_ $$aHasuo, Ichiro$$b2$$eThesis advisor
001002329 8564_ $$uhttps://publications.rwth-aachen.de/record/1002329/files/1002329.pdf$$yOpenAccess
001002329 8564_ $$uhttps://publications.rwth-aachen.de/record/1002329/files/1002329_source.zip$$yRestricted
001002329 909CO $$ooai:publications.rwth-aachen.de:1002329$$pdnbdelivery$$pec_fundedresources$$pVDB$$pdriver$$popen_access$$popenaire
001002329 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
001002329 9141_ $$y2024
001002329 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM04047$$aRWTH Aachen$$b0$$kRWTH
001002329 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM00048$$aRWTH Aachen$$b1$$kRWTH
001002329 9201_ $$0I:(DE-82)121310_20140620$$k121310$$lLehrstuhl für Softwaremodellierung und Verifikation (Informatik 2)$$x0
001002329 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1
001002329 961__ $$c2025-02-12T15:48:58.206904$$x2025-01-15T21:45:00.005195$$z2025-02-12T15:48:58.206904
001002329 9801_ $$aFullTexts
001002329 980__ $$aI:(DE-82)120000_20140620
001002329 980__ $$aI:(DE-82)121310_20140620
001002329 980__ $$aUNRESTRICTED
001002329 980__ $$aVDB
001002329 980__ $$aphd