Industrial hardware and software verification with ACL2
Industrial hardware and software verification with ACL2
复制标题
DOI：
10.1098/rsta.2015.0399
复制
发表时间：
2017-10-13
期刊：
影响因子：
5
通讯作者：
Slobodova, Anna
中科院分区：
文献类型：
--
作者：
Hunt, Warren A., Jr.;Kaufmann, Matt;Slobodova, Anna
自20世纪90年代中期以来，ACL 2定理证明器一直在工业上使用。经常使用ACL 2的公司包括AMD、Centaur Technology、IBM、Intel、Kestrel Institute、Motorola/Freescale、Oracle和Rockwell柯林斯。本文介绍了ACL 2，并重点介绍了ACL 2如何以及为什么在工业中使用。ACL 2非常适合其在众多软件和硬件系统中的工业应用，因为它是一个集成的编程/证明环境，支持ANSI标准Common Lisp编程语言的子集。作为一种编程语言，ACL 2允许编写高效和健壮的程序;作为一种证明器，ACL 2可以是全自动的，但提供了许多功能，允许在不同的抽象层次上进行特定领域的人工指导。ACL 2规范和模型通常作为有效的执行引擎，同时允许形式化的分析和证明的属性。最重要的是，ACL 2还为其他形式化分析工具的开发和验证提供支持。然而，ACL 2并没有仅仅因为其技术特征而进入工业应用。核心ACL 2用户/开发社区有一个共同的愿景，即在适当的时候进行机械化验证，并且自Computational Logic，Inc.已验证堆栈。该社区一直致力于通过承担工业项目来展示该工具的可行性（通常以无法发布太多内容为代价）。本文是主题问题“经验证的可信赖软件系统”的一部分。
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 wellsuited 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 article is part of the themed issue 'Verified trustworthy software systems'.