1. ACL2 Community (accessed January, 2017): ACL2+Books Documentation. Available at
  2. Anna Slobodova, Jared Davis, Sol Swords, and Warren A. Hunt, Jr. (2011): A Flexible Formal Verification Framework for Industrial Scale Validation. In: 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2011, pp. 89–97, doi:10.1109/MEMCOD.2011.5970515.
  3. R. S. Boyer & J S. Moore (1981): Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures. In: The Correctness Problem in Computer Science. Academic Press, London.
  4. David Greve (2006): Parameterized Congruences in ACL2. In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2 '06. ACM, New York, NY, USA, pp. 28–34, doi:10.1145/1217975.1217981.
  5. W. A. Hunt, Jr., M. Kaufmann, R. B. Krug, J S. Moore & E. W. Smith (2005): Meta Reasoning in ACL2. In: J. Hurd & T. Melham: 18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005, Lecture Notes in Computer Science 3603. Springer, pp. 163–178, doi:10.1007/11541868_11.
  6. Matt Kaufmann and J S. Moore (Accessed: 2016): ACL2 home page. (see URL
  7. Matt Kaufmann, J S. Moore, Sandip Ray, and Erik Reeber (2009): Integrating External Deduction Tools with ACL2. Journal of Applied Logic 7(1), pp. 3 – 25, doi:10.1016/j.jal.2007.07.002. Special Issue: Empirically Successful Computerized Reasoning.
  8. Sol Swords (2010): A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover. Department of Computer Sciences, The University of Texas at Austin. Available at
  9. Sol Swords and Jared Davis (2011): Bit-Blasting ACL2 Theorems. In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 84–102, doi:10.4204/EPTCS.70.7.

Comments and questions to:
For website issues: