Weakest precondition reasoning for expected runtimes of randomized algorithms
From MaRDI portal
Recommendations
- Weakest precondition reasoning for expected run-times of probabilistic programs
- Reasoning about Recursive Probabilistic Programs
- Automated recurrence analysis for almost-linear expected-runtime bounds
- Formalising Semantics for Expected Running Time of Probabilistic Programs
- Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
Cited in
(28)- Inferring expected runtimes of probabilistic integer programs using expected sizes
- Automated termination analysis of polynomial probabilistic programs
- Computing expected runtimes for constant probability programs
- Weakest precondition reasoning for expected run-times of probabilistic programs
- Deciding fast termination for probabilistic VASS with nondeterminism
- A Band and Bound Technique for Simple Random Algorithms
- Probabilistic rewriting: normalization, termination, and unique normal forms
- Probabilistic rewriting and asymptotic behaviour: on termination and unique normal forms
- A weakest pre-expectation semantics for mixed-sign expectations
- Tail probabilities for randomized program runtimes via martingales for higher moments
- Foundations for entailment checking in quantitative separation logic
- Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
- Does a Program Yield the Right Distribution?
- Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
- On Lexicographic Proof Rules for Probabilistic Termination
- Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
- Automated tail bound analysis for probabilistic recurrence relations
- MDPs as distribution transformers: affine invariant synthesis for safety objectives
- Probabilistic program verification via inductive synthesis of inductive invariants
- On lexicographic proof rules for probabilistic termination
- From innermost to full almost-sure termination of probabilistic term rewriting
- Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
- Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
- From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity
- Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
- Control-flow refinement for complexity analysis of probabilistic programs in \textsf{KoAT} (short paper)
- A Kleene algebra with tests for union bound reasoning about probabilistic programs
- Latticed \(k\)-induction with an application to probabilistic programs
This page was built for publication: Weakest precondition reasoning for expected runtimes of randomized algorithms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4625651)
