Machines reasoning about machines: 2015

Abstract

Computer hardware and software can be modeled precisely in mathematical logic. If expressed appropriately, these models can be executable, i.e., run on concrete data. This allows them 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 45 year history of the “Boyer-Moore theorem prover,” starting with its use in Edinburgh, Scotland, to prove simple list processing theorems by mathematical induction (e.g., the reverse of the reverse of x is x) to its routine commercial use in the microprocessor industry (e.g., the floating point operations of the Via Nano 64-bit X86 microprocessor are compliant with the IEEE standard). Along the way we will see applications in program verification, models of instruction set architectures including the JVM, and security and information flow. I then list some reasons this project has been successful. The paper also serves as an annotated bibliography of the key stepping stones in the applications of the prover.