% IMPORTANT: The following is UTF-8 encoded. This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.
@MASTERSTHESIS{BeothyElo:1016969,
author = {Beothy-Elo, Emil},
othercontributors = {Katoen, Joost-Pieter and Noll, Thomas and Schroer, Philipp
and Haase, Darion},
title = {{E}ffective quantifier-based reasoning for quantitative
deductive verification},
school = {RWTH Aachen University},
type = {Masterarbeit},
address = {Aachen},
publisher = {RWTH Aachen University},
reportid = {RWTH-2025-07050},
pages = {1 Online-Ressource : Illustrationen},
year = {2025},
note = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
University; Masterarbeit, RWTH Aachen University, 2025},
abstract = {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.},
cin = {121310 / 120000},
ddc = {004},
cid = {$I:(DE-82)121310_20140620$ / $I:(DE-82)120000_20140620$},
typ = {PUB:(DE-HGF)19},
doi = {10.18154/RWTH-2025-07050},
url = {https://publications.rwth-aachen.de/record/1016969},
}
guest ::