ACL2 Support for Floating-Point Computations

Formal methods tools vary widely but generally have logical foundations. For ACL2, a general purpose theorem prover under continuous development since about 1990, having a sound logical foundation is absolutely essential. Many formal tools support execution on concrete data, and ACL2 does so by being compatible with the Common Lisp language: theorems can be proved about Common Lisp functions in the ACL2 subset, and efficient execution is provided by reliance on compiled Common Lisp code. ACL2’s arithmetic is based on a straightforward axiomatization of the rationals and Common Lisp provides exact rational arithmetic. But computation based on exact rational arithmetic is relatively slow, so we have recently added support for floating-point operations in ACL2. The challenge is how to do this while preserving the pre-existing axioms for arithmetic and a large regression suite containing verified theorems and other logical tools contributed and used by the entire ACL2 community. We discuss how we have met these challenges, we discuss the limitations of our support for floating-point operations, and we illustrate the resulting system with examples.