Probabilistic program verification via inductive synthesis of inductive invariants
From MaRDI portal
Recommendations
- Data-Driven Invariant Learning for Probabilistic Programs
- Inductive synthesis for probabilistic programs reaches new horizons
- Linear-invariant generation for probabilistic programs: automated support for proof-based methods
- Verification of Probabilistic Programs
- Counterexample-driven synthesis for probabilistic program sketches
Cites work
- scientific article; zbMATH DE number 700091 (Why is no real title available?)
- scientific article; zbMATH DE number 1538049 (Why is no real title available?)
- scientific article; zbMATH DE number 1884411 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- scientific article; zbMATH DE number 3349291 (Why is no real title available?)
- A lattice-theoretical fixpoint theorem and its applications
- Abstraction, Refinement and Proof for Probabilistic Systems
- Approximate counting in SMT and value estimation for probabilistic programs
- Automated termination analysis of polynomial probabilistic programs
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- Counterexample-guided inductive synthesis for probabilistic systems
- Counterexample-guided polynomial loop invariant generation by Lagrange interpolation
- Data-Driven Invariant Learning for Probabilistic Programs
- Deductive proofs of almost sure persistence and recurrence properties
- Does a Program Yield the Right Distribution?
- Ensuring the reliability of your model checker: interval iteration for Markov decision processes
- Finding polynomial loop invariants for probabilistic programs
- Inductive synthesis for probabilistic programs reaches new horizons
- Latticed \(k\)-induction with an application to probabilistic programs
- Learning probabilistic termination proofs
- Linear-invariant generation for probabilistic programs: automated support for proof-based methods
- Model checking finite-horizon Markov chains with probabilistic inference
- On the hardness of analyzing probabilistic programs
- Optimistic value iteration
- Probabilistic termination: soundness, completeness, and compositionality
- Ranking and repulsing supermartingales for reachability in probabilistic programs
- Sound value iteration
- Stochastic invariants for probabilistic termination
- Symbolic model checking for probabilistic processes
- Synthesizing Probabilistic Invariants via Doob’s Decomposition
- Termination analysis of probabilistic programs through Positivstellensatz's
- Termination of nondeterministic probabilistic programs
- Weakest precondition reasoning for expected run-times of probabilistic programs
- Weakest precondition reasoning for expected runtimes of randomized algorithms
- \textsf{PrIC3}: property directed reachability for MDPs
Cited in
(6)- Quantitative verification with neural networks
- Quantitative verification with neural networks
- From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity
- Quantifier elimination and Craig interpolation: the quantitative way
- MDPs as distribution transformers: affine invariant synthesis for safety objectives
- Data-driven invariant learning for probabilistic programs
This page was built for publication: Probabilistic program verification via inductive synthesis of inductive invariants
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6536145)
