Effective quantifier-based reasoning for quantitative deductive verification

Beothy-Elo, Emil; Haase, Darion; Noll, Thomas; Schroer, Philipp; Katoen, Joost-Pieter

doi:10.18154/RWTH-2025-07050

Effective quantifier-based reasoning for quantitative deductive verification

Beothy-Elo, Emil^RWTH*

2025

Verantwortlichkeitsangabeby Emil Beothy-Elo

ImpressumAachen : RWTH Aachen University 2025

Umfang1 Online-Ressource : Illustrationen

Masterarbeit, RWTH Aachen University, 2025

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Noll, Thomas (Thesis advisor)^RWTH* ; Schroer, Philipp (Consultant)^RWTH* ; Haase, Darion (Consultant)^RWTH*

Tag der mündlichen Prüfung/Habilitation
2025-06-11

Online
DOI: 10.18154/RWTH-2025-07050
URL: https://publications.rwth-aachen.de/record/1016969/files/1016969.pdf

Einrichtungen

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
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.

OpenAccess:
PDF