h1

000998370 001__ 998370
000998370 005__ 20251006114210.0
000998370 0247_ $$2datacite_doi$$a10.18154/RWTH-2024-11340
000998370 037__ $$aRWTH-2024-11340
000998370 041__ $$aEnglish
000998370 082__ $$a004
000998370 1001_ $$0P:(DE-82)IDM05116$$aSchroer, Philipp$$b0$$urwth
000998370 245__ $$aA deductive verifier for probabilistic programs$$cby Philipp Schroer$$honline
000998370 260__ $$aAachen$$bRWTH Aachen University$$c2024
000998370 300__ $$a1 Online-Ressource: Illustrationen
000998370 3367_ $$02$$2EndNote$$aThesis
000998370 3367_ $$0PUB:(DE-HGF)19$$2PUB:(DE-HGF)$$aMaster Thesis$$bmaster$$mmaster
000998370 3367_ $$2BibTeX$$aMASTERSTHESIS
000998370 3367_ $$2DRIVER$$amasterThesis
000998370 3367_ $$2DataCite$$aOutput Types/Supervised Student Publication
000998370 3367_ $$2ORCID$$aSUPERVISED_STUDENT_PUBLICATION
000998370 500__ $$aVeröffentlicht auf dem Publikationsserver der RWTH Aachen University 2024
000998370 502__ $$aMasterarbeit, RWTH Aachen University, 2022$$bMasterarbeit$$cRWTH Aachen University$$d2022$$gFak01$$o2022-01-25
000998370 5203_ $$lger
000998370 520__ $$aWe 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.$$leng
000998370 591__ $$aGermany
000998370 7001_ $$0P:(DE-82)IDM00048$$aKatoen, Joost-Pieter$$b1$$eThesis advisor$$urwth
000998370 7001_ $$0P:(DE-82)066714$$aMüller, Peter$$b2$$eThesis advisor
000998370 7001_ $$0P:(DE-82)IDM04047$$aBatz, Kevin$$b3$$eConsultant$$urwth
000998370 7001_ $$0P:(DE-82)IDM01411$$aKaminski, Benjamin$$b4$$eConsultant$$urwth
000998370 7001_ $$0P:(DE-82)IDM01605$$aMatheja, Christoph$$b5$$eConsultant$$urwth
000998370 8564_ $$uhttps://publications.rwth-aachen.de/record/998370/files/998370.pdf$$yOpenAccess
000998370 909CO $$ooai:publications.rwth-aachen.de:998370$$pdnbdelivery$$pdriver$$pVDB$$popen_access$$popenaire
000998370 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM05116$$aRWTH Aachen$$b0$$kRWTH
000998370 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM00048$$aRWTH Aachen$$b1$$kRWTH
000998370 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM04047$$aRWTH Aachen$$b3$$kRWTH
000998370 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM01411$$aRWTH Aachen$$b4$$kRWTH
000998370 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM01605$$aRWTH Aachen$$b5$$kRWTH
000998370 9141_ $$y2024
000998370 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
000998370 9201_ $$0I:(DE-82)121310_20140620$$k121310$$lLehrstuhl für Softwaremodellierung und Verifikation (Informatik 2)$$x0
000998370 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1
000998370 961__ $$c2024-12-06T08:33:44.688839$$x2024-12-03T09:10:13.755628$$z2024-12-06T08:33:44.688839
000998370 9801_ $$aFullTexts
000998370 980__ $$aI:(DE-82)120000_20140620
000998370 980__ $$aI:(DE-82)121310_20140620
000998370 980__ $$aUNRESTRICTED
000998370 980__ $$aVDB
000998370 980__ $$amaster