ACL2: an industrial strength version of Nqthm

Author

Kaufmann, Matt ; Moore, J. Strother

Author_Institution

Computer Logic Inc., Austin, TX, USA

fYear

1996

fDate

17-21 Jun 1996

Firstpage

23

Lastpage

34

Abstract

ACL2 (“A Computational Logic for Applicative Common Lisp”) is a reimplemented extended version of Boyer and Moore´s (1979, 1988) Nqthm and Kaufmann´s (1988, 1990, 1992) Pc-Nqthm, intended for large-scale verification projects. However, the logic supported by ACL2 is compatible with the applicative subset of Common Lisp. The decision to use an “industrial strength” programming language as the foundation of the mathematical logic is crucial to our advocacy of ACL2 in the application of formal methods to large systems. However, one of the key reasons Nqthm has been so successful, we believe, is its insistence that functions be total. Common Lisp functions are not total and this is one of the reasons Common Lisp is so efficient. This paper explains how we scaled up Nqthm´s logic to Common Lisp, preserving the use of total functions within the logic but achieving Common Lisp execution speeds

Keywords

LISP; formal logic; formal verification; functions; logic programming; programming theory; theorem proving; ACL2; Common Lisp applicative subset; Pc-Nqthm; computational logic; execution speeds; formal methods; industrial-strength programming language; large-scale verification projects; mathematical logic; total functions; Computer applications; Contracts; Hardware; History; Large-scale systems; Logic programming; Mathematical programming; Microprocessors; Software systems; Testing;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Assurance, 1996. COMPASS '96, Systems Integrity. Software Safety. Process Security. Proceedings of the Eleventh Annual Conference on

Conference_Location

Gaithersburg, MD

Print_ISBN

0-7803-3390-X

Type

conf

DOI

10.1109/CMPASS.1996.507872

Filename

507872