Machines Reasoning about Machines
Oct 30, 2002
AbstractComputer hardware and software can be modeled precisely in
mathematical logic. These models can be used as simulation engines.
But symbolic manipulation techniques -- mechanical theorem provers --
can be used to reason about those models. That is, machines can
reason about machines. But how practical is this vision? In turns
out that today researchers in academia and industry are using
mechanical theorem provers to establish interesting facts about
commercial microprocessor designs, including processors by AMD,
Motorola, IBM, Rockwell-Collins and others. 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.
About the SpeakerJ 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-author of the Boyer-Moore
theorem 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.
The views, opinions and assumptions expressed in these videos are those of the presenter and do not necessarily reflect the official policy or position of CERIAS or Purdue University. All content included in these videos, are the property of Purdue University, the presenter and/or the presenter’s organization, and protected by U.S. and international copyright laws. The collection, arrangement and assembly of all content in these videos and on the hosting website exclusive property of Purdue University. You may not copy, reproduce, distribute, publish, display, perform, modify, create derivative works, transmit, or in any other way exploit any part of copyrighted material without permission from CERIAS, Purdue University.