ACL2 2009 is the eighth in the series of workshops on the ACL2 Theorem Prover and Its Applications. The 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, co-authored by Matt Kaufmann and J Strother Moore, is a state-of-the-art automated reasoning system that has been successfully used in academia, government, and industry for specification and verification of computing systems. ACL2 is the most recent incarnation of the Boyer-Moore family of theorem provers, for which Robert Boyer, Matt Kaufmann and J Moore received the 2005 ACM Software System Award. More information about ACL2, including downloads, documentation, relevant books and papers, and previous workshops can be found in the ACL2 Home Page.

ACL2 2009 will be held in Boston, MA, USA on the 11th and 12th of May, 2009. In addition to paper presentations, the workshop is anticipated to include keynote lectures, a panel discussion, and several rump sessions discussing ongoing research. For details about the workshop, follow the links to the left of this page.

News