h1

h2

h3

h4

h5
h6

001     998370
005     20251006114210.0
024 7 _ |2 datacite_doi
|a 10.18154/RWTH-2024-11340
037 _ _ |a RWTH-2024-11340
041 _ _ |a English
082 _ _ |a 004
100 1 _ |0 P:(DE-82)IDM05116
|a Schroer, Philipp
|b 0
|u rwth
245 _ _ |a A deductive verifier for probabilistic programs
|c by Philipp Schroer
|h online
260 _ _ |a Aachen
|b RWTH Aachen University
|c 2024
300 _ _ |a 1 Online-Ressource: Illustrationen
336 7 _ |0 2
|2 EndNote
|a Thesis
336 7 _ |0 PUB:(DE-HGF)19
|2 PUB:(DE-HGF)
|a Master Thesis
|b master
|m master
336 7 _ |2 BibTeX
|a MASTERSTHESIS
336 7 _ |2 DRIVER
|a masterThesis
336 7 _ |2 DataCite
|a Output Types/Supervised Student Publication
336 7 _ |2 ORCID
|a SUPERVISED_STUDENT_PUBLICATION
500 _ _ |a Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2024
502 _ _ |a Masterarbeit, RWTH Aachen University, 2022
|b Masterarbeit
|c RWTH Aachen University
|d 2022
|g Fak01
|o 2022-01-25
520 3 _ |l ger
520 _ _ |a 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.
|l eng
591 _ _ |a Germany
700 1 _ |0 P:(DE-82)IDM00048
|a Katoen, Joost-Pieter
|b 1
|e Thesis advisor
|u rwth
700 1 _ |0 P:(DE-82)066714
|a Müller, Peter
|b 2
|e Thesis advisor
700 1 _ |0 P:(DE-82)IDM04047
|a Batz, Kevin
|b 3
|e Consultant
|u rwth
700 1 _ |0 P:(DE-82)IDM01411
|a Kaminski, Benjamin
|b 4
|e Consultant
|u rwth
700 1 _ |0 P:(DE-82)IDM01605
|a Matheja, Christoph
|b 5
|e Consultant
|u rwth
856 4 _ |u https://publications.rwth-aachen.de/record/998370/files/998370.pdf
|y OpenAccess
909 C O |o oai:publications.rwth-aachen.de:998370
|p openaire
|p open_access
|p VDB
|p driver
|p dnbdelivery
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)IDM05116
|a RWTH Aachen
|b 0
|k RWTH
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)IDM00048
|a RWTH Aachen
|b 1
|k RWTH
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)IDM04047
|a RWTH Aachen
|b 3
|k RWTH
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)IDM01411
|a RWTH Aachen
|b 4
|k RWTH
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)IDM01605
|a RWTH Aachen
|b 5
|k RWTH
914 1 _ |y 2024
915 _ _ |0 StatID:(DE-HGF)0510
|2 StatID
|a OpenAccess
920 1 _ |0 I:(DE-82)121310_20140620
|k 121310
|l Lehrstuhl für Softwaremodellierung und Verifikation (Informatik 2)
|x 0
920 1 _ |0 I:(DE-82)120000_20140620
|k 120000
|l Fachgruppe Informatik
|x 1
980 1 _ |a FullTexts
980 _ _ |a I:(DE-82)120000_20140620
980 _ _ |a I:(DE-82)121310_20140620
980 _ _ |a UNRESTRICTED
980 _ _ |a VDB
980 _ _ |a master

LibraryCollectionCLSMajorCLSMinorLanguageAuthor
Marc 21