Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function

DOI10.1007/978-3-540-73210-5_18MaRDI QIDQ3608890zbMATH OpenOpenAlexFDO

Authors Osman Hasan, Sofiène Tahar

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

zbMATH Keywords

cumulative distribution functionhigher-order-logicHOLinteractive theorem provingprobabilistic systems

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
• 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

Cited in

(6)

• 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
• Formalization of Continuous Probability Distributions
• Reasoning about conditional probabilities in a higher-order-logic theorem prover
• Formalization of the standard uniform random variable

Describes a project that uses

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)