Formal verification of tail distribution bounds in the HOL theorem prover
DOI10.1002/MMA.1055zbMATH Open1167.68053OpenAlexW2006220703MaRDI QIDQ3608329FDOQ3608329
Authors: Osman Hasan, Sofiène Tahar 
Publication date: 4 March 2009
Published in: Mathematical Methods in the Applied Sciences (Search for Journal in Brave)
Full work available at URL: https://spectrum.library.concordia.ca/974500/1/formal_verification_of_tail_distribution.pdf
Recommendations
- Using theorem proving to verify expectation and variance for discrete random variables
- Verification of Expectation Properties for Discrete Random Variables in HOL
- Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function
- Formal reasoning about finite-state discrete-time Markov chains in HOL
- Verified tail bounds for randomized programs
meanvarianceChebyshev inequalityMarkov inequalityautomated theorem provinghigher-order logicprobabilistic analysis of algorithmsdiscrete random variablemechanization of proofs
Inequalities; stochastic orderings (60E15) Analysis of algorithms (68W40) Axioms; other general questions in probability (60A05)
Cites Work
- A theory of type polymorphism in programming
- Title not available (Why is that?)
- Probability and Computing
- A formulation of the simple theory of types
- Title not available (Why is that?)
- Probabilistic guarded commands mechanized in HOL
- Verification of Expectation Properties for Discrete Random Variables in HOL
- Title not available (Why is that?)
- Keplers komplizierter Weg zur Wahrheit: Von neuen Schwierigkeiten, die „Astronomia Nova”︁ zu lesen
- Theorem Proving in Higher Order Logics
Cited In (5)
- Reasoning about conditional probabilities in a higher-order-logic theorem prover
- Using theorem proving to verify expectation and variance for discrete random variables
- Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays
- Verification of Expectation Properties for Discrete Random Variables in HOL
- Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function
Uses Software
This page was built for publication: Formal verification of tail distribution bounds in the HOL theorem prover
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3608329)
