Eleventh International Workshop on the ACL2 Theorem Prover and Its Applications

ACL2 is an industrial-strength theorem prover in the Boyer-Moore family of theorem provers. With an executable logic, support for recursive and constrained functions, and strong support for rewriting and induction, ACL2 is used extensively in academia and industry for the specification and verification of hardware and software systems. The 2005 ACM Software Systems Award was awarded to Robert Boyer, Matt Kaufmann, and J Strother Moore for their work on the Boyer-Moore family of theorem provers.

ACL2 2013 is the eleventh in a series of workshops devoted to ACL2 and its applications. These workshops provide the 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 industry, government, and academia.

ACL2 2013 will be held in Laramie, Wyoming, USA on the 30th and 31st of May, 2013. As in past workshops, ACL2 2013 will feature a mix of technical papers, invited talks, panels, and "rump sessions" that cover the spectrum of activity in the ACL2 community.

Registration is now open. See the registration page for details or click on the button below to register.