Verified tail bounds for randomized programs

DOI10.1007/978-3-319-94821-8_33MaRDI QIDQ1791202zbMATH OpenOpenAlexFDO

Authors Joseph Tassarotti, Robert Harper

Publication date 4 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-94821-8_33

Mathematics Subject Classification ID

Randomized algorithms (68W20) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Probabilistic recurrence relations revisited
• (Probabilistic) recurrence relations revisited
• Proofs of Randomized Algorithms in Coq
• Proofs of randomized algorithms in Coq
• Verified analysis of random binary tree structures

Cited in

(11)

• (Probabilistic) recurrence relations revisited
• Probabilistic Analysis of Binary Sessions
• Foundations for entailment checking in quantitative separation logic
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Verified analysis of random binary tree structures
• A trustful monad for axiomatic reasoning with probability and nondeterminism
• Verified analysis of random binary tree structures
• Computing expected runtimes for constant probability programs
• Tail probabilities for randomized program runtimes via martingales for higher moments
• Formal verification of tail distribution bounds in the HOL theorem prover
• Automated tail bound analysis for probabilistic recurrence relations

Describes a project that uses

Uses Software

• Treaps
• QuickSort Cost
• Coquelicot
• Isabelle/HOL
• Coq

This page was built for publication: Verified tail bounds for randomized programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1791202)