An industrial strength theorem prover for a logic based on Common Lisp
Authors:
- J.S. MooreJMJ.S. Moore
- 1 April 1997
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 23 (4) , 203-213
Abstract
ACL2 is a reimplemented extended version of R.S. Boyer and J.S. Moore's (1979; 1988) Nqthm and M. Kaufmann's (1988) Pc-Nqthm, intended for large scale verification projects. The 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 K/86 microprocessor by Advanced Micro Devices, Inc.Keywords
This publication has 21 references indexed in Scilit:
- VIS: A system for verification and synthesis1996
- ACL2 theorems about commercial microprocessors1996
- Metamathematics, Machines and Gödel's Proof1994
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocolFormal Aspects of Computing, 1994
- Introduction to the OBDD algorithm for the ATP communityJournal of Automated Reasoning, 1994
- Machine checked proofs of the design of a fault-tolerant circuitFormal Aspects of Computing, 1992
- Analytica — A theorem prover in mathematica1992
- Automated correctness proofs of machine code programs for a commercial microprocessor1992
- Functional Instantiation in First-Order Logic1991
- An approach to systems verificationJournal of Automated Reasoning, 1989