h1

h2

h3

h4

h5
h6

001     1016969
005     20250929074706.0
024 7 _ |2 datacite_doi
|a 10.18154/RWTH-2025-07050
037 _ _ |a RWTH-2025-07050
041 _ _ |a English
082 _ _ |a 004
100 1 _ |0 P:(DE-82)1018016
|a Beothy-Elo, Emil
|b 0
|u rwth
245 _ _ |a Effective quantifier-based reasoning for quantitative deductive verification
|c by Emil Beothy-Elo
|h online
260 _ _ |a Aachen
|b RWTH Aachen University
|c 2025
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
502 _ _ |a Masterarbeit, RWTH Aachen University, 2025
|b Masterarbeit
|c RWTH Aachen University
|d 2025
|g Fak01
|o 2025-06-11
520 3 _ |l ger
520 _ _ |a Caesar 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.
|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)IDM01580
|a Noll, Thomas
|b 2
|e Thesis advisor
|u rwth
700 1 _ |0 P:(DE-82)IDM05116
|a Schroer, Philipp
|b 3
|e Consultant
|u rwth
700 1 _ |0 P:(DE-82)IDM06494
|a Haase, Darion
|b 4
|e Consultant
|u rwth
856 4 _ |u https://publications.rwth-aachen.de/record/1016969/files/1016969.pdf
|y OpenAccess
909 C O |o oai:publications.rwth-aachen.de:1016969
|p openaire
|p open_access
|p VDB
|p driver
|p dnbdelivery
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)1018016
|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)IDM01580
|a RWTH Aachen
|b 2
|k RWTH
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)IDM05116
|a RWTH Aachen
|b 3
|k RWTH
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)IDM06494
|a RWTH Aachen
|b 4
|k RWTH
914 1 _ |y 2025
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