ACL2 copyright, license, sponsorship

ACL2 Version 6.3 -- A Computational Logic for Applicative Common Lisp Copyright (C) 2013, Regents of the University of Texas

This version of ACL2 is a descendent 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: and Department of Computer Science University of Texas at Austin Austin, TX 78701 U.S.A.

Please also see acknowledgments.