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

zbMATH Keywords

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

Mathematics Subject Classification ID

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)

Latticed \(k\)-induction with an application to probabilistic programs ⋮ Foundations for entailment checking in quantitative separation logic

Uses Software

• z3
• FOCI
• PySMT
• KoAT

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