Jasmin Christian Blanchette & Tobias Nipkow (2010):
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder.
In: Matt Kaufmann & Lawrence C. Paulson: ITP,
Lecture Notes in Computer Science 6172.
Springer,
pp. 131–146,
doi:10.1007/978-3-642-14052-5_11.
Available at http://dx.doi.org/10.1007/978-3-642-14052-5.
R. S. Boyer & J S. Moore (1979):
A Computational Logic.
Academic Press,
New York.
Achim D. Brucker & Burkhart Wolff (2004):
Symbolic Test Case Generation for Primitive Recursive Functions.
In: Jens Grabowski & Brian Nielsen: FATES,
Lecture Notes in Computer Science 3395.
Springer,
pp. 16–32.
Available at http://dx.doi.org/10.1007/978-3-540-31848-4_2.
Matthieu Carlier & Catherine Dubois (2008):
Functional Testing in the Focal Environment.
In: Bernhard Beckert & Reiner Hähnle: TAP,
Lecture Notes in Computer Science 4966.
Springer,
pp. 84–98.
Available at http://dx.doi.org/10.1007/978-3-540-79124-9_7.
Harsh Raju Chamarthi & Peter C. Dillinger:
Data Definition framework in ACL2 Sedan.
In preparation.
Koen Claessen & John Hughes (2000):
QuickCheck: a lightweight tool for random testing of Haskell programs.
In: ICFP,
pp. 268–279.
Available at http://doi.acm.org/10.1145/351240.351266.
Jeremy Dick & Alain Faivre (1993):
Automating the Generation and Sequencing of Test Cases from Model-Based Specifications.
In: Jim Woodcock & Peter Gorm Larsen: FME,
Lecture Notes in Computer Science 670.
Springer,
pp. 268–284.
Available at http://dx.doi.org/10.1007/BFb0024651.
Peter C. Dillinger, Panagiotis Manolios, Daron Vroon & J. Strother Moore (2007):
ACL2s: "The ACL2 Sedan".
Electr. Notes Theor. Comput. Sci. 174(2),
pp. 3–18.
Available at http://dx.doi.org/10.1016/j.entcs.2006.09.018.
Peter Dybjer, Qiao Haiyan & Makoto Takeyama (2003):
Combining Testing and Proving in Dependent Type Theory.
In: David A. Basin & Burkhart Wolff: TPHOLs,
Lecture Notes in Computer Science 2758.
Springer,
pp. 188–203.
Available at http://dx.doi.org/10.1007/10930755_12.
John D. Erickson (2007):
Backtracking and Induction in ACL2.
In: Seventh International Workshop on the ACL2 Theorem prover and its Applications (ACL2 '07).
Ruben Gamboa, John Cowles & Jeff Van Baalen (2003):
Using ACL2 Arrays to Formalize Matrix Algebra.
In: Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03).
Marie-Claude Gaudel (1995):
Testing Can Be Formal, Too.
In: Peter D. Mosses, Mogens Nielsen & Michael I. Schwartzbach: TAPSOFT,
Lecture Notes in Computer Science 915.
Springer,
pp. 82–96.
Available at http://dx.doi.org/10.1007/3-540-59293-8_188.
Warren A. Hunt Jr. & Erik Reeber (2006):
A SAT-based procedure for verifying finite state machines in ACL2.
In: Panagiotis Manolios & Matthew Wilding: ACL2.
ACM,
pp. 127–135.
Available at http://doi.acm.org/10.1145/1217975.1218001.
Matt Kaufmann, Panagiotis Manolios & J Strother Moore (2000):
Computer-Aided Reasoning: An Approach.
Kluwer Academic Publishers.
Matt Kaufmann & J Strother Moore:
Backtrack hint documentation.
See URL http://www.cs.utexas.edu/users/moore/acl2/current/BACKTRACK.html.
Matt Kaufmann & J Strother Moore:
BDD documentation.
See URL http://www.cs.utexas.edu/users/moore/acl2/current/BDD.html.
Matt Kaufmann & J Strother Moore:
Computed hints documentation.
See URL http://www.cs.utexas.edu/users/moore/acl2/current/COMPUTED-HINTS.html.
Matt Kaufmann & J Strother Moore:
Override-hints documentation.
See URL http://www.cs.utexas.edu/users/moore/acl2/current/OVERRIDE-HINTS.html.
Matt Kaufmann & J Strother Moore:
Waterfall documentation.
See URL http://www.cs.utexas.edu/users/moore/acl2/current/HINTS-AND-THE-WATERFALL.html.
Robert B. Krug:
Arithmetic-5 Library.
See books/arithmetic-5/README in ACL2 regression suite.
Panagiotis Manolios & Sudarshan K. Srinivasan (2005):
Verification of executable pipelined machines with bit-level interfaces.
In: ICCAD.
IEEE Computer Society,
pp. 855–862.
Panagiotis Manolios & Sudarshan K. Srinivasan (2006):
A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures.
J. Autom. Reasoning 37(1-2),
pp. 93–116.
Available at http://dx.doi.org/10.1007/s10817-006-9035-0.
Panagiotis Manolios & Daron Vroon (2006):
Termination Analysis with Calling Context Graphs.
In: Thomas Ball & Robert B. Jones: CAV,
Lecture Notes in Computer Science 4144.
Springer,
pp. 401–414.
Available at http://dx.doi.org/10.1007/11817963_36.
Sam Owre (2006):
Random Testing in PVS.
In: Workshop on Automated Formal Methods(AFM) 10,
Seattle, WA, USA.
Alexander Spiridonov & Sarfraz Khurshid (2007):
Automatic generation of counterexamples for ACL2 using Alloy.
In: Seventh International Workshop on the ACL2 Theorem prover and its Applications (ACL2 '07).
Rob Sumners (2002):
Checking ACL2 Theorems via SAT Checking.
In: Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02).
T. Weber:
SAT-Based Finite Model Generation for Higher-Order Logic.
Ph.D. thesis, Dept. of Informatics, T.U.München, 2008..
eptcs@eptcs.org