Machines Reasoning about Machines - 2015

Computer hardware and software can be modelled precisely in mathematical logic.  If expressed appropriately, these models can be executable.  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 Project", starting with its use in Edinburgh to prove simple theorems by mathematical induction about list processing (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.