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.
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.
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.
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.
Matt Kaufmann and J S. Moore (Accessed: 2016):
ACL2 home page.
(see URL http://www.cs.utexas.edu/users/moore/acl2).
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.
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 http://hdl.handle.net/2152/ETD-UT-2010-12-2210.
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.
eptcs@eptcs.org