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 in ACL2 and the other theorem provers in the Boyer-Moore family.

Since its inception, the ACL2 Workshop series has been the major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications.

The first ACL2 Workshop, then known as The ACL2 Wizard Workshop was held in the Texas Governor's Room of the Texas Union at the University of Texas at Austin. That first workshop resulted in two books, Computer-Aided Reasining: An Approach and Computer-Aided Reasining: ACL2 Case Studies, both published by Kluwer in 2000.

Since then, workshops have been held on an irregular schedule, typically 18 months between workshops. Most workshops have taken place in Austin, TX, the birthplace of the Boyer-Moore family of theorem provers. Some workshops have been held at other locations, usually to co-locate with other major conferences of interest to the ACL2 community, e.g., European Joint Conferences on Theory and Practice of Software (ETAPS) in 2002, Computer-Aided Verification (CAV) in 2003, Federated Logic Conference (FLoC) in 2006, 2010, and 2014, and Formal Methods in Computer-Aided Design (FMCAD) in 2004, 2007, 2011, 2015, and 2018.

Proceedings from the ACL2 Workshop series have been published with EPTCS in 2011, 2013, 2014, 2015, and 2017; with Springer LNCS 6172 in 2010; and with the ACM digital library in 2006 and 2009.

You can find out more information about the ACL2 Workshops at the official page of the workshop series.