Latticed k-Induction with an Application to Probabilistic Programs

Lecture notes in computer science, pp. 524–549

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.

Authors 6

1. Kevin Batz corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   RWTH Aachen University

2. Mingshuai Chen corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   RWTH Aachen University

3. Benjamin Lucien Kaminski corresponding Aachen

   University College London · RWTH Aachen University

   Affiliation as printed

   University College London, London, UK

   RWTH Aachen University

4. Joost-Pieter Katoen corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   RWTH Aachen University

5. Christoph Matheja corresponding

   ETH Zurich

   Affiliation as printed

   ETH Zürich, Zürich, Switzerland

   ETH Zurich Zurich Switzerland

6. Philipp Schröer Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   RWTH Aachen, University, Aachen, Germany