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