Computer hardware and software can be modeled 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 turns out that researchers in academia and industry are using mechanical theorem provers to prove important theorems about commercial microprocessor designs, including processors by AMD, Motorola, IBM, Rockwell-Collins and others. Some of these microprocessor models execute at 90% the speed of C and have had important functional properties verified. In addition, we are modeling the Java Virtual Machine and are proving theorems about JVM methods. I will describe these and other recent applications of an industrial-strength version of the Boyer-Moore theorem prover.

Biography:

J Strother Moore holds the Admiral B.R. Inman Centennial Chair in Computing Theory at the University of Texas at Austin. He is also chair of the department. He is the author of many books and papers on automated theorem proving and mechanical verification of computing systems. Along with Boyer he is a co-authortheorem prover and the Boyer-Moore fast string searching algorithm. With Matt Kaufmann he is the co-author of the ACL2 theorem prover. Moore got his PhD from the University of Edinburgh in 1973 and his BS from MIT in 1970. Moore was a founder of Computational Logic, Inc., and served as its chief scientist for ten years. He and Bob Boyer were awarded the 1991 Current Prize in Automatic Theorem Proving by the American Mathematical Society. In 1999 they were awarded the Herbrand Award for their work in automatic theorem proving. Moore is a Fellow of the American Association for Artificial Intelligence.