ACL2定理证明器学术盛会，聚焦工业级自动化推理技术
Proceedings 19th International Workshop on the ACL2 Theorem Prover and Its Applications
- 汇集全球用户分享ACL2定理证明器的最新研究与应用
- 该系统属博耶-穆尔家族，获2005年ACM软件系统奖
- 适合形式化验证、程序正确性验证领域研究人员
ACL2研讨会系列是使用ACL2定理证明系统的用户展示相关研究和技术应用的主要技术论坛。ACL2是博耶-穆尔定理证明器家族中的最新一代工业级自动化推理系统。博耶、考夫曼和穆尔因在ACL2及其他博耶-穆尔家族定理证明器方面的工作，于2005年获得ACM软件系统奖。
原文摘要 · Abstract (English)
The ACL2 Workshop series is the major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications. ACL2 is an industrial-strength automated reasoning system, the latest in the Boyer-Moore family of theorem provers. The 2005 ACM Software System Award was awarded to Boyer, Kaufmann, and Moore for their work on ACL2 and the other theorem provers in the Boyer-Moore family.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。