Speaker: Peter Manolios
Affiliation: University of Texas
Date: 4/12/01
Time and Location: 4:15 PM, B11 Kimball Hall
Title: Combining Theorem Proving and Model Checking for
         the Verification of Reactive Systems
Abstract: 

Reactive systems are non-terminating systems that maintain an ongoing interaction with their environment. Examples include network protocols, pipelined machines, cache coherence protocols, and distributed transaction systems. Such systems are becoming ubiquitous and as a society we are increasingly dependent on their correct behavior. Reactive systems are notoriously difficult to design and mechanical verification appears to be the only reliable way of ensuring their correctness. In fact, companies such as AMD, IBM, Rockwell Collins, Intel, and Motorola, among others, are currently applying formal methods to manage the complexity of their systems.

Model checking and related algorithms can be used on restricted classes of reactive systems to automatically determine if a system satisfies its specification. However, systems of interest are often too large (perhaps infinite-state) or irregular to be verified automatically. Theorem proving, and ACL2 (a programming language, logic, and theorem prover) in particular, has been successfully applied to industrial problems that are infinite-state and beyond the capabilities of model checking, but significant human interaction is required. I will describe a novel approach that allows us to combine the strengths of both approaches. Theorem proving is used to reduce, in a property preserving way, the original system to a simpler system which can then be handled with automatic methods. I will explain the underlying theory, its implementation in ACL2, and its application to the verification of several reactive systems, including pipelined
machines and communications protocols.