Machines Reasoning about Machines
Prof. J Strother Moore
Recorded 07 June 2011 in Lausanne, Vaud, Switzerland
Event: SuRI - I&C - Summer Research Institute
Computer hardware and software can be modeled precisely in mathematical logic. If expressed appropriately, these models can be executable. An appropriate logic is an axiomatically formalized functional programming language. This allows models to be used as simulation engines or rapid prototypes. But because they are formal they can be manipulated by symbolic means: theorems can be proved about them, directly, with mechanical theorem provers.
But how practical is this vision of machines reasoning about machines? In this highly personal talk, I will describe the 40 year history of the Boyer-Moore Project and discuss progress toward making formal verification practical. Among other examples I will describe important theorems about commercial microprocessor designs, including parts of processors by AMD, Motorola, IBM, Rockwell-Collins and others. Some of these microprocessor models execute at 90% the speed of C models and have had important functional properties verified. In addition, I will describe a model of the Java Virtual Machine, including class loading and bytecode verification and the proofs of theorems about JVM methods.
Watched 16427 times.Watch