Latticed k-Induction with an Application to Probabilistic Programs

Abstract

Abstract We revisit two well-established verification techniques,k-inductionandbounded model checking(BMC), in the more general setting of fixed point theory over complete lattices. Our main theoretical contribution islatticed k-induction, which (i) generalizes classicalk-induction for verifying transition systems, (ii) generalizes Park induction for bounding fixed points of monotonic maps on complete lattices, and (iii) extends from naturalskto transfinite ordinals $$\kappa $$ κ , thus yielding $$\kappa $$ κ -induction. The lattice-theoretic understanding ofk-induction and BMC enables us to apply both techniques to thefully 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.