Subject: [lyall@larch.lcs.mit.edu: Seminar by J Strother Moore]
From: Be Blackburn (be@theory.lcs.mit.edu)
Date: Thu Oct 11 2001 - 14:59:35 EDT
------- Start of forwarded message -------
Return-Path: <lyall@larch.lcs.mit.edu>
Date: Thu, 11 Oct 2001 14:50:31 EDT
From: Neena Lyall <lyall@larch.lcs.mit.edu>
To: seminars@lcs.mit.edu, fac-res@hq.lcs.mit.edu, grads@hq.lcs.mit.edu,
ugrads@hq.lcs.mit.edu
Cc: help-teach@lcs.mit.edu, assistants@ai.mit.edu
Subject: Seminar by J Strother Moore
Machines Reasoning about Machines
J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Tuesday, October 16, 2001 in NE43-518
Refreshments at 1:45 PM followed by the talk at 2:00 PM
Abstract:
Computer hardware and software can be described precisely in mathematical
logic. Mechanical theorem proving techniques can be used to reason about
those descriptions. But how practical is this vision? In this talk I
describe how one particular theorem prover, ACL2, is being applied to
industrial verification projects. ACL2, developed by Matt Kaufmann and me,
is a descendent of the Boyer-Moore theorem prover. With ACL2, the RTL the
elementary floating point arithmetic circuits on the AMD Athlon was proved to
be compliant with the IEEE 754 floating-point standard. This was done at AMD
as part of the design cycle, before fabrication. Bugs in well-tested designs
were found and fixed. Pipelined machine models, DSPs, secure co-processors,
avionics microprocessors and other devices have been described in bit- and
cycle-accurate ways and proved to have important functional properties. ACL2
is also being applied to software, including Java classes that involve
arithmetic, objects, dynamic method resolution, pointer chasing,
multi-threading, and synchronization via monitors. ACL2 can also be used to
prove the correctness of theorem proving code and has been so used in
industry to develop trusted CAD tools and at Argonne National Labs to build
trusted theorem provers.
Biography:
J Strother Moore holds the Admiral B.R. Inman Centennial Chair in
Computing Theory at the University of Texas at Austin. 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.
Host: Mike Ernst
------- End of forwarded message -------
This archive was generated by hypermail 2b28 : Thu Oct 11 2001 - 15:11:27 EDT