This volume contains a selection of papers presented at the 17th
International Workshop on the ACL2 Theorem Prover and its Applications (ACL2
2022). The workshops are the premier technical forum for presenting research
and experiences related to ACL2.

该论文集收录了 ACL2 定理证明器及其应用方面的研究和经验，讨论 ACL2 定理证明器在技术论坛和应用方面的作用。

ACL2 定理证明器及其应用国际研讨会第十七届会议论文集

Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications

This volume contains the proceedings of the Thirteenth International Workshop
on the ACL2 Theorem Prover and Its Applications, ACL2 2015, a two-day workshop
held in Austin, Texas, USA, on October 1-2, 2015. ACL2 workshops occur at
approximately 18-month intervals and provide a major technical forum for
researchers to present and discuss improvements and extensions to the theorem
prover, comparisons of ACL2 with other systems, and applications of ACL2 in
formal verification.
ACL2 is a state-of-the-art automated reasoning system that has been
successfully applied in academia, government, and industry for specification
and verification of computing systems and in teaching computer science courses.
In 2005, Boyer, Kaufmann, and Moore were awarded the 2005 ACM Software System
Award for their work on ACL2 and the other theorem provers in the Boyer-Moore
family.

该论文介绍了一个自动化推理系统 ACL2 定理证明器，其应用包括计算系统规范和验证，形式验证等，Boyer-Moore 家族的成员在 ACL2 Theorem Prover 研究和发展中做出重要贡献。