Latticed \(k\)-induction with an application to probabilistic programs
DOI10.1007/978-3-030-81688-9_25zbMath1493.68204arXiv2105.14100OpenAlexW3186609013MaRDI QIDQ832288
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Kevin Batz, Mingshuai Chen, Christoph Matheja, Philipp Schröer
Publication date: 25 March 2022
Full work available at URL: https://arxiv.org/abs/2105.14100
bounded model checkingfixed-point theoryquantitative verification\(k\)-inductionprobabilistic programs
Complete lattices, completions (06B23) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Automatic analysis of DMA races using model checking and \(k\)-induction
- Latticed \(k\)-induction with an application to probabilistic programs
- A probabilistic PDL
- Fixed point theorems and semantics: A folk tale
- Constructive versions of Tarski's fixed point theorems
- On the hardness of analyzing probabilistic programs
- Bounded model checking for probabilistic programs
- Inferring expected runtimes of probabilistic integer programs using expected sizes
- 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
- Bounded model checking of infinite state systems
- An interpolating theorem prover
- A lattice-theoretical fixpoint theorem and its applications
- A counterexample-guided abstraction-refinement framework for markov decision processes
- SAT-Based Model Checking without Unrolling
- Complete Lattices and Up-To Techniques
- Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
- Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
- Synthesizing Probabilistic Invariants via Doob’s Decomposition
- Abstraction, Refinement and Proof for Probabilistic Systems
- Linear-Invariant Generation for Probabilistic Programs:
- Finding Polynomial Loop Invariants for Probabilistic Programs
- Randomized mutual exclusion algorithms revisited
- Enhancements of the bisimulation proof method
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Computer Aided Verification
- Bounded model checking using satisfiability solving
- Sound value iteration
- Interpolating strong induction
This page was built for publication: Latticed \(k\)-induction with an application to probabilistic programs
