Machines Reasoning about Machines
Event details
| Date | 07.06.2011 |
| Hour | 10:15 |
| Speaker | Prof. J Strother Moore, University of Texas at Austin, Keynote Speaker |
| Location |
CO-1
|
| Category | Conferences - Seminars |
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. Prof. J Strother Moore's homepage
Practical information
- General public
- Free