Probabilistic Analysis in HOL

Description

Realistic analysis of many systems requires availability of accurate methods and tools. Formal methods such as model checking and theorem proving have seen intereset in attempting problems involving modeling of random phenomenon and random behavior of complex systems. In our research, we focus on the formalization of basic underlying mathematics essential for reasoning about probabilities, random variables, markov chains, reliability and Information theory. We develop methedologies and tools for application to engineering problems. Following are three main active projects in our group at this time.

Current Projects

• Formal Probabilistic Risk Assessment using Theorem Proving
• Formal Dynamic Dependability Analysis using HOL Theorem Proving
• Information-Theoretic Analysis using Theorem Proving
• Formal Probabilistic Analysis of Wireless Sensors in HOL
• Formal Analysis of Information Flow Using Min-Entropy and Belief Min-Entropy
• Formalization of Continuous Time Markov Chains with Applications in Queuing Theory
• Formalization of Normal Random Variables
• Formalization of the M/M/1 Queue in HOL

Past Projects

• Formal Reliability Analysis Using HOL Theorem Prover
• Formal Markov Chain Analysis Using HOL Theorem Prover
• Probabilistic Analysis in the HOL Theorem Prover