ACL2 Seminar, Feb. 16, 2011

Formal Analysis for Trustworthy Large-scale Computing

Sandip Ray

Computer errors and malfunctions can cost millions of dollars to our
economy, lead to loss of human life, and severely subvert our national
security.  On the other hand, modern computing systems are getting
more and more complex and error-prone, with bugs increasingly
difficult to detect and diagnose.  As computer systems become even
more pervasive it is critical that they can be trusted to behave
reliably, predictably, securely, and according to specification.

This talk will focus on approaches based on formal verification, i.e.,
mechanized mathematical analysis, to meet the challenges of
trustworthy computing.  The scale and complexity of modern computing
systems demand high scalability in the reasoning approach.  I will
argue that in order for formal analysis to be effective it must be
applied judiciously through hierarchical, disciplined reasoning
frameworks.  I will show examples of such reasoning frameworks,
discuss the underlying general principles behind their design, and
explain how their use can ameliorate verification cost.

Our frameworks have found application in academia and industry for
analysis of diverse computing systems, ranging from hardware designs
to Java programs.  I will draw from these experiences to identify some
key challenges in large-scale pervasive use of formal analysis and
point to possible approaches for overcoming them through cooperation
between design and verification research.