Machines Reasoning about Machines

J Strother Moore


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 for all of the elementary floating point arithmetic circuits on the AMD Athlon was proved to be compliant with the IEEE 754 floating-point standard. 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.

©2002-2018 U.C. Regents