• Top
    • Documentation
      • Xdoc
      • ACL2-doc
      • Recursion-and-induction
      • Loop$-primer
      • Operational-semantics
      • Pointers
      • Doc
      • Documentation-copyright
      • Course-materials
      • Publications
        • Pub-books
        • Pub-videos
          • Pub-papers
          • Pub-summary
          • Pub-related-web-sites
          • Pub-slides
        • Args
        • ACL2-doc-summary
        • Finding-documentation
        • Broken-link
        • Doc-terminal-test-2
        • Doc-terminal-test-1
      • Books
      • Boolean-reasoning
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Publications

    Pub-videos

    Videos about ACL2

    Videos For Learning ACL2

    • The Tenth Summer School on Formal Techniques (2021) included a series of videos teaching ACL2:
      • Welcome
      • Video 0
      • Video 1
      • Video 2
      • Video 3
      • Video 4
      • Video 5
      • Video 6a
      • Video 6b
      • Video 7
      The Summer School webpage includes additional supplementary materials.

    Videos About ACL2 and Its Applications

    • What's New in ACL2, from the ACL2 2018 Workshop (Matt Kaufmann and Holly Bell, 2018)
    • Formal Verification of Cryptographic Code (Eric Smith, 2018)
    • Formal Verification of JubJub R1CS Gadgets (Alessandro Coglio, Eric McCarthy, Eric Smith, 2021)
    • Protocol Analysis Using Real Analysis in ACL2 (Max von Hippel, 2023)
    • An ACL2-based x86-ISA Specification (Warren Hunt, 2024)
    • Demo of the ACL2-Doc Emacs-based documentation browser (also see its documentation).
    • An Integration of Axiomatic Set Theory with ACL2 (Matt Kaufmann): Part 1, Part 2, and Part 3.