Latticed k-Induction with an Application to Probabilistic Programs
2021
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 \(\kappa \), thus yielding \(\kappa \)-induction.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
66
References
0
Citations
NaN
KQI