Latticed k-induction with an application to probabilistic programs

DOI10.1007/978-3-030-81688-9_25zbMATH Open1493.68204arXiv2105.14100OpenAlexW3186609013MaRDI QIDQ832288FDOQ832288

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

Publication date: 25 March 2022

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.

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

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

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)

Cites Work

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

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

Uses Software

• z3
• FOCI
• PySMT
• KoAT

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)