Gast ::
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