Abstract

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 workshop will feature technical papers, invited talks, and rump sessions discussing ongoing research. We invite submissions of papers on any topic related to ACL2 and its applications, and we strongly encourage submissions related to other theorem provers or formal methods that are of interest to the ACL2 community. Suggested topics include but are not limited to new results in the following areas. - Software or hardware verification with ACL2 - Formalizations of mathematics in ACL2 - Libraries and tools for ACL2 - User interfaces for ACL2 - Novel uses of ACL2 - Experiences with ACL2 in the classroom - Reports of and proposals for improvements of ACL2 - Comparisons with other theorem provers - Comparisons with other programming or specification languages - Challenge problems and their solutions - Foundational issues related to ACL2 - Implementations connecting ACL2 with other systems