An industrial strength theorem prover for a logic based on Common Lisp
- 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
- https://doi.org/10.1109/32.588534
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:
- Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methodsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- VIS: A system for verification and synthesisLecture Notes in Computer Science, 1996
- ACL2 theorems about commercial microprocessorsPublished by Springer Nature ,1996
- Metamathematics, Machines and Gödel's ProofPublished by Cambridge University Press (CUP) ,1994
- 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 mathematicaPublished by Springer Nature ,1992
- Automated correctness proofs of machine code programs for a commercial microprocessorPublished by Springer Nature ,1992
- Functional Instantiation in First-Order LogicPublished by Elsevier ,1991