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