Speaker: Waqar Ahmed
Title: Formal Dependability Analysis using Theorem Proving

Abstract:

Dependability is an umbrella concept that subsumes many key properties
about a system, including reliability, maintainability, safety,
availability, confidentiality, and integrity. Various dependability
modeling techniques have been developed to effectively capture the failure
characteristics of systems over time. Traditionally, dependability models
are analyzed using paper-and-pencil proof methods and computer based
simulation tools but their results cannot be trusted due to their inherent
inaccuracy limitations. To overcome these limitations, we propose to
leverage upon the recent developments in probabilistic analysis support in
higher-order-logic theorem proving to conduct accurate and rigorous
dependability analysis.
This talk has been divided in two parts. Firstly, I will discuss about the
dependability and its formalization in HOL4. The second part is about
computing the dependability using ACL2, which particularly covers porting
the exponential function to ACL2 using HOL4/ACL2 link and the verification
of error bound property of MacLaurin series for exponential function.