An Introduction to ACL2

Included here are the following.

• Slides in pdf format for two 1.25 hour talks in a UT CS graduate class (April 2015 and again in April 2016).
• A gzipped tarfile with supporting materials (ACL2 input files and corresponding logs) referenced in those slides.

Of related interest are two recent talks given at the workshop on Verified Trustworthy Software Systems, Specialist Meeting, London, UK, April 2016:

• Prof. Warren Hunt (speaker), Shilpi Goel, and Matt Kaufmann of UT Austin: Analysis of x86 Application and System Programs via Machine-Code Verification
• Anna Slobodova of Centaur Technology, reporting on joint work with Jared Davis, Sol Swords, Warren Hunt, and Matt Kaufmann: Formal Analysis of x86 Designs at Centaur Technology