Large 00988

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 1836 times.