Latticed k-induction with an application to probabilistic programs

DOI10.1007/978-3-030-81688-9_25MaRDI QIDQ832288zbMATH OpenOpenAlexFDO

Authors Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2105.14100

zbMATH Keywords

bounded model checkingfixed-point theoryquantitative verification\(k\)-inductionprobabilistic programs

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Complete lattices, completions (06B23)

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 $kappa$, thus yielding $kappa$-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.

Recommendations

• Bounded model checking for probabilistic programs
• Verification of Probabilistic Programs
• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
• Validation of Stochastic Systems
• The Lattice-Theoretic Essence of Property Directed Reachability Analysis

Cites work

• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1884411 (Why is no real title available?)
• scientific article; zbMATH DE number 2102695 (Why is no real title available?)
• scientific article; zbMATH DE number 783754 (Why is no real title available?)
• scientific article; zbMATH DE number 3349291 (Why is no real title available?)
• A counterexample-guided abstraction-refinement framework for Markov decision processes
• A lattice-theoretical fixpoint theorem and its applications
• A probabilistic PDL
• Abstraction, Refinement and Proof for Probabilistic Systems
• An interpolating theorem prover
• Automatic analysis of DMA races using model checking and k-induction
• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
• Bounded model checking for probabilistic programs
• Bounded model checking of infinite state systems
• Bounded model checking using satisfiability solving
• Complete Lattices and Up-To Techniques
• Constructive versions of Tarski's fixed point theorems
• Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
• Enhancements of the bisimulation proof method
• Ensuring the reliability of your model checker: interval iteration for Markov decision processes
• Finding polynomial loop invariants for probabilistic programs
• Fixed point theorems and semantics: A folk tale
• Fixpoint theory -- upside down
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Interpolating strong induction
• Interpolation and SAT-based model checking.
• Latticed \(k\)-induction with an application to probabilistic programs
• Linear-invariant generation for probabilistic programs: automated support for proof-based methods
• On the hardness of analyzing probabilistic programs
• Optimistic value iteration
• Probabilistic guarded commands mechanized in HOL
• Randomized mutual exclusion algorithms revisited
• SAT-Based Model Checking without Unrolling
• Sound value iteration
• Synthesizing Probabilistic Invariants via Doob’s Decomposition
• Tools and Algorithms for the Construction and Analysis of Systems
• Weakest precondition reasoning for expected runtimes of randomized algorithms
• \textsf{PrIC3}: property directed reachability for MDPs

Cited in

(7)

• Latticed \(k\)-induction with an application to probabilistic programs
• Foundations for entailment checking in quantitative separation logic
• The Lattice-Theoretic Essence of Property Directed Reachability Analysis
• Does a Program Yield the Right Distribution?
• MDPs as distribution transformers: affine invariant synthesis for safety objectives
• Certificates for probabilistic pushdown automata via optimistic value iteration
• Probabilistic program verification via inductive synthesis of inductive invariants

Describes a project that uses

Uses Software

• KoAT
• PySMT
• FOCI
• z3

This page was built for publication: Latticed \(k\)-induction with an application to probabilistic programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832288)