Workshops
The ACL2 Workshop Series.
The ACL2 Workshop series consists of conferences that are held
regularly, as listed below.
In 2010, the ACL2 Workshop did a one-time merger with TPHOLs to form the
first International Conference on Interactive Theorem Proving (ITP). Such a
merger may occur again, but whether or not that happens, the ACL2 community is
encouraged to participate in ITP. Other conferences of particular interest to
the ACL2 community include CAV (Computer Aided Verification) and FMCAD
(Formal Methods in Computer Aided Design).
- ACL2
Workshop 2025: May 12-13, 2025, Austin, Texas, USA and also online.
- ACL2
Workshop 2023: November 13-14, 2023, Austin, Texas, USA and also
online.
- ACL2
Workshop 2022: May 26-27, 2022, Austin, Texas, USA and also online.
- ACL2 Workshop 2020: May 28-29,
2020 (held online via video streaming).
- ACL2
Workshop 2018: November 5-6, 2018, Austin, Texas, USA.
- ACL2 Workshop 2017: May 22 - 23, 2017, Austin, Texas, USA.
- ACL2
Workshop 2015: October 1-2, 2015, Austin, Texas, USA. (Co-located with FMCAD
2015.)
- ACL2 Workshop 2014: July 12-13,
2014, Vienna, Austria, as an ITP-affiliated workshop of FLoC (part of the Vienna Summer of Logic).
- ACL2 Workshop 2013:
May 30-31, 2013, University of Wyoming, Laramie, Wyoming, USA.
- ACL2
Workshop 2011: November 3-4, 2011, Austin, Texas, USA. (Co-located with
FMCAD 2011.)
- ITP 2010:
Int'l Conference on Interactive Theorem Proving (ITP) 2010: July 11-14,
2010, Edinburgh, Scotland; part of FLoC
2010.
- ACL2
Workshop 2009: May 11-12, 2009, Boston, Massachusetts, USA. (Proceedings
available from ACM Digital Library.)
- ACL2 Workshop 2007:
November 15-16, 2007, Austin, Texas, USA.
- ACL2 Workshop 2006:
August 15-16, 2006, Seattle, Washington, USA. (Proceedings
available from ACM Digital Library.)
- ACL2
Workshop 2004: November 18-19, 2004, Austin, Texas, USA.
- ACL2
Workshop 2003: July 13-14, 2003, Boulder, Colorado, USA.
- ACL2
Workshop 2002: April 8-9, 2002, Grenoble, France.
- ACL2
Workshop 2000: October 30-31, 2000, Austin, Texas, USA.
- ACL2
Workshop 1999: March 29-31, 1999, Austin, Texas, USA.
List of past ACL2 Workshop slogans:
- 1999: It ain't over til the last Q.E.D.
- 2000: Just prove it.
- 2002: Accumulated Persistence
- 2003: No software too trivial. No error too obscure.
- 2004: Defun starts here
- 2006: ACM Software Systems Award Winner!
- 2007: Save the world. Use make-event.
- 2009: None
- 2011: We aim to prove
- 2013: Pain is temporary; theorems are forever.
- 2014: I love the smell of parentheses in the morning.
- 2015: 25 years of rewriting history
- 2017: In Proof We Trust
- 2018: Sometimes you feel like alist, sometimes you don't
- 2020: (defaxiom acl2-2020 'Damn nil. Full speed
ahead!' (not (lexorder 'acl2 'covid-19)))
- 2022: supporting (in-theory ...) local events
- 2023: Certifiable
- 2025: I'm sorry, Dave: I'm afraid I can't prove that.
Jared Davis, Keshav Kini, and Andrew Walter have graciously supplied a
listing of bibtex entries for the ACL2 workshops through 2023 (would be
nice if extended past 2023; any volunteers?).
ACL2 input files (certifiable books) from the preceding
workshops are available in the ACL2+Books GitHub repository,
specifically, in its subdirectory
for workshop contributions.
