An industrial strength theorem prover for a logic based on Common Lisp

Author

Kaufmann, Matt ; Moore, J.S.

Author_Institution

Motorola Inc., Austin, TX, USA

Volume

23

Issue

4

fYear

1997

fDate

4/1/1997 12:00:00 AM

Firstpage

203

Lastpage

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_K86 microprocessor by Advanced Micro Devices, Inc

Keywords

LISP; digital signal processing chips; floating point arithmetic; program verification; theorem proving; ACL2; AMD5_K86 microprocessor; Advanced Micro Devices; Common Lisp; Motorola CAP digital signal processing chip; Nqthm; Pc-Nqthm; floating point division algorithm; formal logic; formal models; industrial strength programming language; industrial strength theorem prover; large applicative subset; large scale verification projects; proof of correctness; reimplemented extended version; Automatic logic units; Digital signal processing chips; Functional programming; Kernel; Large-scale systems; Logic devices; Logic programming; Mathematics; Microprocessors; Signal processing algorithms;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.588534

Filename

588534