Latticed k-Induction with an Application to Probabilistic Programs

6Citations
Citations of this article
2Readers
Mendeley users who have this article in their library.

This article is free to access.

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.

Cite

CITATION STYLE

APA

Batz, K., Chen, M., Kaminski, B. L., Katoen, J. P., Matheja, C., & Schröer, P. (2021). Latticed k-Induction with an Application to Probabilistic Programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12760 LNCS, pp. 524–549). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-81688-9_25

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free