h1

001016969 001__ 1016969
001016969 005__ 20250929074706.0
001016969 0247_ $$2datacite_doi$$a10.18154/RWTH-2025-07050
001016969 037__ $$aRWTH-2025-07050
001016969 041__ $$aEnglish
001016969 082__ $$a004
001016969 1001_ $$0P:(DE-82)1018016$$aBeothy-Elo, Emil$$b0$$urwth
001016969 245__ $$aEffective quantifier-based reasoning for quantitative deductive verification$$cby Emil Beothy-Elo$$honline
001016969 260__ $$aAachen$$bRWTH Aachen University$$c2025
001016969 300__ $$a1 Online-Ressource : Illustrationen
001016969 3367_ $$02$$2EndNote$$aThesis
001016969 3367_ $$0PUB:(DE-HGF)19$$2PUB:(DE-HGF)$$aMaster Thesis$$bmaster$$mmaster
001016969 3367_ $$2BibTeX$$aMASTERSTHESIS
001016969 3367_ $$2DRIVER$$amasterThesis
001016969 3367_ $$2DataCite$$aOutput Types/Supervised Student Publication
001016969 3367_ $$2ORCID$$aSUPERVISED_STUDENT_PUBLICATION
001016969 500__ $$aVeröffentlicht auf dem Publikationsserver der RWTH Aachen University
001016969 502__ $$aMasterarbeit, RWTH Aachen University, 2025$$bMasterarbeit$$cRWTH Aachen University$$d2025$$gFak01$$o2025-06-11
001016969 5203_ $$lger
001016969 520__ $$aCaesar is a deductive verifier for probabilistic programs. It builds on modern SMT solvers to automatically check if probabilistic programs conform to their specification. This high degree of automation sometimes comes at the cost of brittle verification. Seemingly unrelated changes in the input program can cause the verifier to hang and verification to fail. These instabilities are often caused by quantifiers that are used in axioms to describe the relevant theories for verification. A common problem here are matching loops - an ill-behaved set of quantifiers that can cause an infinite number of quantifier instantiations by themselves. A large contributor of matching loops are user-defined recursive functions. A common approach taken by other verifiers is to encode such functions as limited functions, limiting the number of recursive instantiations and avoiding matching loops by construction. While they have been proven to be effective, there is little information available about them and they lacked a formal treatment. We present and formally define different limited function encodings used by other verifiers, and subsequently prove that these transformations are sound. Furthermore, we examine how one of the encodings can be modified to obtain finite and constructible counterexamples involving recursive functions. The presented encodings are implemented in Caesar. We provide guidance on the subtleties that are required for the encodings to work well in practice. Our evaluation shows that the implemented encodings are very effective in eliminating brittleness for problematic programs in Caesar's test suite.$$leng
001016969 591__ $$aGermany
001016969 7001_ $$0P:(DE-82)IDM00048$$aKatoen, Joost-Pieter$$b1$$eThesis advisor$$urwth
001016969 7001_ $$0P:(DE-82)IDM01580$$aNoll, Thomas$$b2$$eThesis advisor$$urwth
001016969 7001_ $$0P:(DE-82)IDM05116$$aSchroer, Philipp$$b3$$eConsultant$$urwth
001016969 7001_ $$0P:(DE-82)IDM06494$$aHaase, Darion$$b4$$eConsultant$$urwth
001016969 8564_ $$uhttps://publications.rwth-aachen.de/record/1016969/files/1016969.pdf$$yOpenAccess
001016969 909CO $$ooai:publications.rwth-aachen.de:1016969$$pdnbdelivery$$pdriver$$pVDB$$popen_access$$popenaire
001016969 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)1018016$$aRWTH Aachen$$b0$$kRWTH
001016969 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM00048$$aRWTH Aachen$$b1$$kRWTH
001016969 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM01580$$aRWTH Aachen$$b2$$kRWTH
001016969 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM05116$$aRWTH Aachen$$b3$$kRWTH
001016969 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM06494$$aRWTH Aachen$$b4$$kRWTH
001016969 9141_ $$y2025
001016969 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
001016969 9201_ $$0I:(DE-82)121310_20140620$$k121310$$lLehrstuhl für Softwaremodellierung und Verifikation (Informatik 2)$$x0
001016969 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1
001016969 961__ $$c2025-09-08T10:51:25.468865$$x2025-08-19T15:18:04.689937$$z2025-09-08T10:51:25.468865
001016969 9801_ $$aFullTexts
001016969 980__ $$aI:(DE-82)120000_20140620
001016969 980__ $$aI:(DE-82)121310_20140620
001016969 980__ $$aUNRESTRICTED
001016969 980__ $$aVDB
001016969 980__ $$amaster