Session Chair: M.Y. Vardi.

Speaker: John Rushby (SRI International).

Title: Automated Deduction and Formal Methods.

Abstract: Just as computational fluid dynamics uses calculation to examine aerofoil designs, so automated deduction allows specifications and designs for computer systems to be explored and verified through formal calculations. For this approach to be useful, automated deduction must provide methods that are effective for the type and scale of examples that arise in practical applications, and that yield information that is helpful to designers.

Using examples from verifications undertaken by myself and my colleagues in the areas of fault tolerance, protocols, and hardware, I will describe some of the capabilities that we have found useful or necessary. At the lower levels, these include decision procedures for several theories including equality, real and integer linear arithmetic, fast propositional simplification, rewriting, rich typing mechanisms, and the integration of all these. At the higher levels, they include user-directed control strategies, integration of theorem proving with model checking, and automated assistance in the construction of abstractions and invariants.

I will close by speculating on future possibilities, and suggesting some challenging examples.

Biographical Sketch: John Rushby is a program director in the Computer Science Laboratory of SRI International in Menlo Park California, where he leads a research program in formal methods and dependable systems. His group develops mechanized formal verification systems (the latest is called PVS), and applies them to problems in computer security, hardware design, and safety-critical and fault-tolerant systems. PVS is being used in industrial projects applying formal methods and automated verification to aerospace problems at Allied Signal, Honeywell, JPL, Lockheed Martin, and Rockwell-Collins.

Dr. Rushby joined SRI in 1983 and served as Director of its Computer Science Laboratory from 1986 to 1990. Prior to that, he held academic positions at the Universities of Manchester and Newcastle upon Tyne in England. He received BSc and PhD degrees in computing science from the University of Newcastle upon Tyne in 1971 and 1977, respectively. He serves on the program committees for several forthcoming conferences (e.g., Compass, DCCA, FME, and LICS) and is an associate editor for the journals Communications of the ACM and Formal Aspects of Computing. He is the author of the section on formal methods for the FAA Digital Systems Validation Handbook (the guidelines for aircraft certification).