The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.04 - April (1997 vol.23)
pp: 203-213
ABSTRACT
<p><b>Abstract</b>—ACL2 is a reimplemented extended version of Boyer and Moore's Nqthm and Kaufmann's Pc-Nqthm, intended for large scale verification projects. This paper deals primarily with how we scaled up Nqthm's logic to an "industrial strength" programming language—namely, a large applicative subset of Common Lisp—while preserving the use of total functions within the logic. This makes it possible to run formal models efficiently while keeping the logic simple. We enumerate many other important features of ACL2 and we briefly summarize two industrial applications: a model of the Motorola CAP digital signal processing chip and the proof of the correctness of the kernel of the floating point division algorithm on the AMD5<sub><it>K</it></sub>86 microprocessor by Advanced Micro Devices, Inc.</p>
INDEX TERMS
Formal verification, automatic theorem proving, computational logic, partial functions, total functions, type checking, microcode verification, floating point division, digital signal processing.
CITATION
Matt Kaufmann, J S. Moore, "An Industrial Strength Theorem Prover for a Logic Based on Common Lisp", IEEE Transactions on Software Engineering, vol.23, no. 4, pp. 203-213, April 1997, doi:10.1109/32.588534
17 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool