This directory contains material about ACL2 presented by J Moore on 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.

The files here are:

• Industrial Use of a Mechanical Theorem Prover
• talk1.pdf
• talk1.lisp
• talk1.session-log
• An Industrially Useful Prover
• talk2.pdf
• talk2.lisp
• talk2.session-log

The *.pdf files are the slides from the two talks. Each talk included some demonstrations of ACL2. Each talk included several demonstrations of a live ACL2 Version 7.4 session. The scripts for each demo are in the *.lisp files, which consist of ACL2 commands, definitions, theorems, etc., which were submitted to ACL2 during the demos. The slides have occasional headers named ``Demo 1'', ``Demo 2'', etc., and each corresponds to a sequences of commands in the talk1 or talk2 lisp files. The two *.session-log files show the entire sessions (user input and ACL2 output). We expect the scripts will re-play in future ACL2 versions.