% 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”.
@PHDTHESIS{Batz:1002329,
author = {Batz, Kevin},
othercontributors = {Katoen, Joost-Pieter and Hasuo, Ichiro},
title = {{A}utomated deductive verification of probabilistic
programs},
school = {RWTH Aachen University},
type = {Dissertation},
address = {Aachen},
publisher = {RWTH Aachen University},
reportid = {RWTH-2025-00473},
pages = {1 Online-Ressource : Illustrationen},
year = {2024},
note = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
University 2025; Dissertation, RWTH Aachen University, 2024},
abstract = {We study both foundational and practical aspects of the
automated deductive verification of discrete probabilistic
programs. Our special emphasis is on the verification of
possibly unbounded loops by quantitative loop invariants. We
build upon Kozen's, McIver $\&$ Morgan's, and Kaminski's
weakest preexpectation calculus for reasoning about expected
outcomes such as the probability of terminating in some
postcondition or the expected final value of a program
variable. The weakest preexpectation calculus replaces
predicates from classical program verification by more
general expectations --- functions mapping program states to
numbers instead of truth values. We study a syntax for
specifying expectations, providing a foundation for
automated deductive probabilistic program verifiers. We
prove that our syntax is expressive and hence obtain a
relatively complete verification system for reasoning about
expected outcomes. We then present three different
approaches for automating the verification of bounds on
expected outcomes of linear loops, all of which combine
weakest preexpectation reasoning with Satisfiability Modulo
Theories (SMT) techniques: 1. We revisit two
well-established verification techniques for transition
systems, k-induction and bounded model checking (BMC), in
the more general setting of bounding least fixpoints of
functions over complete lattices, yielding latticed
k-induction and latticed BMC. Instantiating our latticed
techniques with the weakest preexpectation calculus enables
the fully automatic verification of linear loops taken from
the literature. 2. We present a counterexample-guided
inductive synthesis approach for the synthesis of
quantitative loop invariants. This enables the fully
automatic verification of bounds on both expected outcomes
and expected runtimes. Our implementation synthesizes
quantitative invariants of various linear loops taken from
the literature, can beat state-of-the-art probabilistic
model checkers on finite-state programs, and is competitive
with modern tools dedicated to invariant synthesis or
expected runtime reasoning. 3. We present PrIC3 --- the
first truly quantitative extension of the state-of-the-art
qualitative symbolic model checking algorithm IC3 to
symbolic model checking of Markov decision processes. By
marrying PrIC3 with the weakest preexpectation calculus, we
obtain a symbolic model checking algorithm for probabilistic
programs. Alongside, we present an implementation of PrIC3
featuring IC3-specific techniques such as generalization.},
cin = {121310 / 120000},
ddc = {004},
cid = {$I:(DE-82)121310_20140620$ / $I:(DE-82)120000_20140620$},
pnm = {FRAPPANT - Formal Reasoning About Probabilistic Programs:
Breaking New Ground for Automation (787914)},
pid = {G:(EU-Grant)787914},
typ = {PUB:(DE-HGF)11},
doi = {10.18154/RWTH-2025-00473},
url = {https://publications.rwth-aachen.de/record/1002329},
}
guest ::