Using Theorem Proving with Algorithmic Techniques for Large-scale System Verification

S. Ray

Ph.D. Oral Proposal, Department of Computer Sciences, University of Texas at Austin, November 2003.

Abstract

We propose to write a thesis on using theorem proving with algorithmic techniques for verification of large scale computer systems. Large-scale computer systems tend to have a non-terminating computation, and reasoning about such systems involves exhibiting some temporal property of the system. For large system models, automatic verification of non-trivial temporal properties is often infeasible, because of the state explosion problem. Theorem proving has a better potential to scale up to large designs, but it often requires considerable user assistance to guide the proof. We consider an intermediate approach, using theorem proving to verify correspondence between executions of a concrete system design and its abstraction, and then using automated analysis to verify the temporal properties of abstractions. We explore the logical issues and problems involved in the use of automated analysis on abstractions verified by a theorem prover. We propose to implement tools and techniques that provide a reasonable amount of automation in the verification process. Further, we plan to demonstrate our techniques on verification of multiprocessor system models, and specifically focus on synchronization protocols, cache coherence, and pipelined architecture of realistic systems. We use ACL2 (a programming language, logic, and theorem prover) to illustrate our techniques.

Relevant files