|
|
|---|
|
|
|
|---|
W. A. Hunt, Jr., M. Kaufmann, J S. Moore, and A. Slobodova, “Industrial
hardware and software verification with ACL2” in P. Gardner,
P. O'Hearn, M. Gordon, G. Morrisett and F. B. Schneider, editors),
Verified Trustworthy Software Systems, Philosophical Transactions A,
Royal Society Publishing, 374, DOI 10.1098/rsta.2015.0399, September,
2017.
Relevance: how ACL2 is used in industry, and why
Abstract
The ACL2 theorem prover has seen sustained industrial use since the mid-1990s. Companies that have used ACL2 regularly include AMD, Centaur Technology, IBM, Intel, Kestrel Institute, Motorola/Freescale, Oracle and Rockwell Collins. This paper introduces ACL2 and focuses on how and why ACL2 is used in industry. ACL2 is well-suited to its industrial application to numerous software and hardware systems, because it is an integrated programming/proof environment supporting a subset of the ANSI standard Common Lisp programming language. As a programming language ACL2 permits the coding of efficient and robust programs; as a prover ACL2 can be fully automatic but provides many features permitting domain-specific human-supplied guidance at various levels of abstraction. ACL2 specifications and models often serve as efficient execution engines for the modelled artefacts while permitting formal analysis and proof of properties. Crucially, ACL2 also provides support for the development and verification of other formal analysis tools. However, ACL2 did not find its way into industrial use merely because of its technical features. The core ACL2 user/development community has a shared vision of making mechanized verification routine when appropriate and has been committed to this vision for the quarter century since the Computational Logic, Inc., Verified Stack. The community has focused on demonstrating the viability of the tool by taking on industrial projects (often at the expense of not being able to publish much).
This is does not discuss operational semantics per se but instead focuses on how ACL2 is used in industry and how ACL2 gained traction in industrial use. The paper discusses how ACL2 is used at Centaur Technology, Inc. When a previously verified module of a microprocessor design is modified by the designers and checked back in to the data base, ACL2 is run that night to attempt to verify the modified design, “bugs introduced today are detected tonight and fixed tomorrow.” The Centaur design and verification teams were acquired by Intel in 2021 and ACL2 continues to be so used at Intel. In addition the paper describes features of ACL2 (and of the ACL2 community of users) that are particularly important to industry.