Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function

DOI10.1007/978-3-540-73210-5_18zbMATH Open1213.68380OpenAlexW1595825122MaRDI QIDQ3608890FDOQ3608890

Sofiène Tahar, Osman Hasan

Publication date: 6 March 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73210-5_18

Recommendations

• Verification of Expectation Properties for Discrete Random Variables in HOL
• Formal verification of tail distribution bounds in the HOL theorem prover
• Using theorem proving to verify expectation and variance for discrete random variables
• Formalization of the standard uniform random variable
• Reasoning about conditional probabilities in a higher-order-logic theorem prover

zbMATH Keywords

cumulative distribution functionHOLinteractive theorem provingprobabilistic systemshigher-order-logic

Mathematics Subject Classification ID

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

Cited In (6)

• Reasoning about conditional probabilities in a higher-order-logic theorem prover
• Formalization of the standard uniform random variable
• Formalization of Continuous Probability Distributions
• Using theorem proving to verify expectation and variance for discrete random variables
• Verification of Expectation Properties for Discrete Random Variables in HOL
• Formal verification of tail distribution bounds in the HOL theorem prover

Uses Software

• IBAL

This page was built for publication: Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function

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