Latticed k-Induction with an Application to Probabilistic Programs
OPEN ACCESS
Author / Producer
Date
2021
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
We revisit two well-established verification techniques, k-induction and bounded model checking (BMC), in the more general setting of fixed point theory over complete lattices. Our main theoretical contribution is latticed k-induction, which (i) generalizes classical k-induction for verifying transition systems, (ii) generalizes Park induction for bounding fixed points of monotonic maps on complete lattices, and (iii) extends from naturals k to transfinite ordinals κ , thus yielding κ -induction.
The lattice-theoretic understanding of k-induction and BMC enables us to apply both techniques to the fully automatic verification of infinite-state probabilistic programs. Our prototypical implementation manages to automatically verify non-trivial specifications for probabilistic programs taken from the literature that—using existing techniques—cannot be verified without synthesizing a stronger inductive invariant first.
Permanent link
Publication status
published
External links
Book title
Computer Aided Verification
Journal / series
Volume
12760
Pages / Article No.
524 - 549
Publisher
Springer
Event
33rd International Conference on Computer-Aided Verification (CAV 2021)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
k-induction; Bounded model checking; Fixed point theory; Probabilistic programs; Quantitative verification
Organisational unit
03653 - Müller, Peter / Müller, Peter