• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
        • Gentle-introduction-to-ACL2-programming
        • ACL2-tutorial
        • About-ACL2
          • Recursion-and-induction
          • Operational-semantics
          • Soundness
          • Release-notes
          • Version
          • Acknowledgments
          • Pre-built-binary-distributions
          • Common-lisp
          • Git-quick-start
          • Copyright
            • Documentation-copyright
          • Building-ACL2
          • ACL2-help
          • Bibliography
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • About-ACL2

Copyright

ACL2 copyright, license, sponsorship

This topic provides information about copyright, license, authorship, and sponsorship of the ACL2 system. For information about copyright and authorship of documentation, see documentation-copyright, which notes that there are many documentation authors.

ACL2 Version 8.6 — A Computational Logic for Applicative Common Lisp

Copyright (C) 2025, Regents of the University of Texas

This version of ACL2 is a descendant of ACL2 Version 1.9, Copyright (C) 1997 Computational Logic, Inc. See the documentation topic NOTE-2-0.

This program is free software; you can redistribute it and/or modify it under the terms of the LICENSE file distributed with ACL2.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the LICENSE for more details.

Written by: Matt Kaufmann and J Strother Moore
email: Kaufmann@cs.utexas.edu and Moore@cs.utexas.edu
Department of Computer Science
University of Texas at Austin
Austin, TX 78712 U.S.A.

Please also see acknowledgments.

Subtopics

Documentation-copyright
Copyright and authorship of documentation