Formal verification of tail distribution bounds in the HOL theorem prover

DOI10.1002/MMA.1055MaRDI QIDQ3608329zbMATHOpenAlexFDO

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

zbMATH Keywords

meanvarianceChebyshev inequalityMarkov inequalityautomated theorem provinghigher-order logicprobabilistic analysis of algorithmsdiscrete random variablemechanization of proofs

Mathematics Subject Classification ID

Inequalities; stochastic orderings (60E15) Analysis of algorithms (68W40) Axioms; other general questions in probability (60A05)

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

Cites work

• scientific article; zbMATH DE number 1259143 (Why is no real title available?)
• scientific article; zbMATH DE number 1927425 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A formulation of the simple theory of types
• A theory of type polymorphism in programming
• Keplers komplizierter Weg zur Wahrheit: Von neuen Schwierigkeiten, die „Astronomia Nova”︁ zu lesen
• Probabilistic guarded commands mechanized in HOL
• Probability and Computing
• Theorem Proving in Higher Order Logics
• Verification of Expectation Properties for Discrete Random Variables in HOL

Cited in

(5)

• Verification of Expectation Properties for Discrete Random Variables in HOL
• Using theorem proving to verify expectation and variance for discrete random variables
• Reasoning about conditional probabilities in a higher-order-logic theorem prover
• Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function
• Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays

Describes a project that uses

Uses Software

• ML
• VESTA

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)