J Strother Moore - Department of Computer Sciences, University of Texas at Austin
Students: Spring 2024, unless noted otherwise, sessions will be virtual on Zoom.
Machines Reasoning about Machines
Oct 30, 2002
Abstract
Computer hardware and software can be modeled precisely inmathematical 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 Speaker
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.
Ways to Watch
