Using theorem proving to verify expectation and variance for discrete random variables

DOI10.1007/S10817-008-9113-6MaRDI QIDQ1040780zbMATH OpenOpenAlexFDO

Authors Osman Hasan, Sofiène Tahar

Publication date 25 November 2009

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://spectrum.library.concordia.ca/974506/1/using_theorem_proving_to_verify_expectation.pdf

zbMATH Keywords

Coupon collector's problemhigher-order-logicHOL theorem proverprobabilistic analysisprobability theorystatistical properties

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification of Expectation Properties for Discrete Random Variables in HOL
• Formal verification of tail distribution bounds in the HOL theorem prover
• Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function
• Formalization of the standard uniform random variable
• Formalization of normal random variables in HOL

Cites work

• A formulation of the simple theory of types
• A stochastic process on the hypercube with applications to peer-to-peer networks
• A theory of type polymorphism in programming
• Automata, Languages and Programming
• Coalescing times for IID random variables with applications to population biology
• Elementary Probability
• Formalization of Continuous Probability Distributions
• scientific article; zbMATH DE number 3815002 (Why is no real title available?)
• scientific article; zbMATH DE number 3954145 (Why is no real title available?)
• scientific article; zbMATH DE number 3544999 (Why is no real title available?)
• scientific article; zbMATH DE number 1259143 (Why is no real title available?)
• scientific article; zbMATH DE number 1161555 (Why is no real title available?)
• scientific article; zbMATH DE number 1927425 (Why is no real title available?)
• scientific article; zbMATH DE number 765034 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 958048 (Why is no real title available?)
• Keplers komplizierter Weg zur Wahrheit: Von neuen Schwierigkeiten, die „Astronomia Nova”︁ zu lesen
• Modern cryptography: theory and practice
• Probabilistic guarded commands mechanized in HOL
• Probability and Computing
• Proofs of Randomized Algorithms in Coq
• Theorem Proving in Higher Order Logics
• Theoretical Aspects of Computing – ICTAC 2005
• Verification of Expectation Properties for Discrete Random Variables in HOL
• Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function

Cited in

(9)

• Formalization of Shannon's theorems
• On the formalization of gamma function in HOL
• Formalization of normal random variables in HOL
• Verification of Expectation Properties for Discrete Random Variables in HOL
• Formal verification of tail distribution bounds in the HOL theorem prover
• Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function
• A formal study of Boolean games with random formulas as payoff functions
• Formal probabilistic analysis of detection properties in wireless sensor networks
• Formalization of the standard uniform random variable

Describes a project that uses

Uses Software

• VESTA
• VESTA
• ML
• HOL

This page was built for publication: Using theorem proving to verify expectation and variance for discrete random variables

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