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.4 — A Computational Logic for Applicative Common Lisp
Copyright (C) 2022, 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.