Machines Reasoning about Machines

Add to your list(s) Download to your calendar using vCal

• J Strother Moore, Professor Emeritus University of Texas
• Friday 15 May 2015, 11:00-12:00
• Huxley Room 308.

If you have a question about this talk, please contact Clare E Drysdale.

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 to prove simple theorems by mathematical induction about list processing (e.g., the reverse of the reverse of x is x) to its routine use in the microprocessor industry (e.g., the floating point operatios 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

This talk is part of the Clare E Drysdale's list series.

This talk is included in these lists:

• Huxley Room 308

Note that ex-directory lists are not shown.