Probabilistic program verification via inductive synthesis of inductive invariants
From MaRDI portal
Publication:6536145
DOI10.1007/978-3-031-30820-8_25zbMATH Open1547.68112MaRDI QIDQ6536145
Benjamin Lucien Kaminski, J.-P. Katoen, Mingshuai Chen, Sebastian Junges, Kevin Batz, Christoph Matheja
Publication date: 5 April 2024
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Learning probabilistic termination proofs
- Latticed \(k\)-induction with an application to probabilistic programs
- Model checking finite-horizon Markov chains with probabilistic inference
- Approximate counting in SMT and value estimation for probabilistic programs
- Counterexample-guided polynomial loop invariant generation by Lagrange interpolation
- On the hardness of analyzing probabilistic programs
- Counterexample-guided inductive synthesis for probabilistic systems
- Inductive synthesis for probabilistic programs reaches new horizons
- Ensuring the reliability of your model checker: interval iteration for Markov decision processes
- Optimistic value iteration
- \textsf{PrIC3}: property directed reachability for MDPs
- Automated termination analysis of polynomial probabilistic programs
- Deductive proofs of almost sure persistence and recurrence properties
- Termination of nondeterministic probabilistic programs
- A lattice-theoretical fixpoint theorem and its applications
- Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
- Probabilistic termination: soundness, completeness, and compositionality
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- Symbolic model checking for probabilistic processes
- Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
- Termination Analysis of Probabilistic Programs Through Positivstellensatz’s
- 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
- Stochastic invariants for probabilistic termination
- Sound value iteration
- Ranking and repulsing supermartingales for reachability in probabilistic programs
- Data-Driven Invariant Learning for Probabilistic Programs
- Does a Program Yield the Right Distribution?
Related Items (1)
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)
