Probabilistic program verification via inductive synthesis of inductive invariants
type: Item
instance of: scholarly article
title: Probabilistic program verification via inductive synthesis of inductive invariants
zbMATH Open document ID: 1547.68112
DOI: 10.1007/978-3-031-30820-8_25
author: Kevin Batz
author: Mingshuai Chen
author: Sebastian Junges
author: Benjamin Lucien Kaminski
author: Joost-Pieter Katoen
author: Christoph Matheja
publication date: 2024-04-05T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 7827817
MaRDI profile type: Publication
cites work: Learning probabilistic termination proofs
cites work: Q4518905
cites work: Inductive synthesis for probabilistic programs reaches new horizons
cites work: Symbolic model checking for probabilistic processes
cites work: Q5322945
cites work: Ensuring the reliability of your model checker: interval iteration for Markov decision processes
cites work: Data-Driven Invariant Learning for Probabilistic Programs
cites work: Synthesizing Probabilistic Invariants via Doob’s Decomposition
cites work: Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
cites work: Latticed \(k\)-induction with an application to probabilistic programs
cites work: \textsf{PrIC3}: property directed reachability for MDPs
cites work: Counterexample-guided inductive synthesis for probabilistic systems
cites work: Deductive proofs of almost sure persistence and recurrence properties
cites work: Termination Analysis of Probabilistic Programs Through Positivstellensatz’s
cites work: Stochastic invariants for probabilistic termination
cites work: Does a Program Yield the Right Distribution?
cites work: Counterexample-guided polynomial loop invariant generation by Lagrange interpolation
cites work: Approximate counting in SMT and value estimation for probabilistic programs
cites work: Q4798031
cites work: Finding Polynomial Loop Invariants for Probabilistic Programs
cites work: Probabilistic termination: soundness, completeness, and compositionality
cites work: Termination of nondeterministic probabilistic programs
cites work: Optimistic value iteration
cites work: Model checking finite-horizon Markov chains with probabilistic inference
cites work: On the hardness of analyzing probabilistic programs
cites work: Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
cites work: Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
cites work: Linear-Invariant Generation for Probabilistic Programs:
cites work: Abstraction, Refinement and Proof for Probabilistic Systems
cites work: Automated termination analysis of polynomial probabilistic programs
cites work: Q5624635
cites work: Q4315289
cites work: Sound value iteration
cites work: Ranking and repulsing supermartingales for reachability in probabilistic programs
cites work: A lattice-theoretical fixpoint theorem and its applications
description: scientific article; zbMATH DE number 7827817