Talks
Some talks about ACL2
The list below contains links to talks about ACL2. This list may
grow over time. Please email the ACL2-help mailing list if you find a
broken link or if you care to contribute another link to a talk (or simply
make the changes yourself if you have permission to do so on GitHub).
- Links to several introductory/overview talks on ACL2 may be found on the
page
of talks by Matt Kaufmann, including a
general introductory talk on ACL2 by Matt Kaufmann and J Moore from
2006.
- Several introductory/overview talks on ACL2 by J Moore:
- Two
talks given July 6 and 7, 2017, at the Big Proof workshop at the
Isaac Newton Institute for Mathematical Sciences in Cambridge, England. The
first talk focuses on the role of mechanized proof,specifically ACL2, to
verify hardware and software of interest to industry. The second talk
touches upon how the ACL2 prover works, how the user directs it, and some of
the features of particular importance to its industrial applications.
- Industrial
Hardware and Software Verification with ACL2, presented at the Royal
Society, London, in April, 2016 (co-authored with Warren A. Hunt, Jr., Matt
Kaufmann, and Anna Slobodova).
- This page for Mechanized
Operational Semantics contains links not only to talks given at the
Marktoberdorf Summer School (Germany, August, 2008) but also to supplemental
materials.
- The ``Talks'' section of Warren Hunt's home
page has an annotated list of links to several talks about the use of ACL2
for hardware specification and verification.
Note that many talks are also available from the ACL2
Workshops pages and on the University of Texas
ACL2 Seminar page.
