##
Formal Probabilistic and Statistical Analysis using Higher-Order Logic

### Sofiene Tahar

Probabilistic and statistical analysis is a tool of fundamental importance
to virtually all scientists and engineers as they often have to deal with
systems that exhibit random or unpredictable elements. Traditionally,
computer simulation techniques are used to perform probabilistic analysis.
However, they provide less accurate results and cannot handle large-scale
problems due to their enormous computer processing time requirements. To
overcome these limitations, we propose to perform formal probabilistic and
statistical analysis using higher-order logic theorem proving. We provide
a framework for the formalization of both discrete and continuous random
variables and the ability to formally verify system's probabilistic and
statistical properties. The analysis carried out in this way is free from
any approximation or precision issues due to the mathematical nature of
the models and the inherent soundness of the theorem proving approach. In
order to illustrate the practical effectiveness of the proposed framework,
we present the probabilistic analysis of four examples across three
application areas: the Coupon Collector's problem (software), the
Stop-and-Wait protocol (telecommunications), the reliability of memory
arrays (microelectronics), and floating-point error analysis (computer
hardware).