Seventh International Workshop on the ACL2 Theorem Prover and its Applications
Used extensively both in industry and academia, ACL2 is an industrial-strength theorem prover in the Boyer-Moore tradition. Like other provers in this family, it features an executable logic, a recursive definitional principle, and strong support for rewriting and induction. In addition, ACL2 includes many features that address scalability, such as support for modular proof development, constrained functions, fast and applicative destructive data structures, and specialized inference methods. Robert Boyer, Matt Kaufmann, and J Strother Moore were awarded the 2005 ACM Software Systems Award for their work on the Boyer-Moore family of theorem provers.
ACL2 2007 is the seventh in a series of workshops that occur approximately every 18 months. 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 2007 will be held in Austin, Texas on November 15th-16th, 2007, in conjunction with FMCAD 2007. Additionally, ACL2 2007 will feature a graduate student seminar, which will include presentations and discussions of Ph.D. topics and issues related to careers involving ACL2 in academia, industry, or government.