# Integrating Testing and Interactive Theorem Proving

Harsh Chamarthi, Peter C. Dillinger, Matt Kaufmann, and Panagiotis Manolios.

*ACL2*, 2011.

# Abstract

Using an interactive theorem prover to reason about programs involves
a sequence of interactions where the user challenges the theorem
prover with conjectures. Invariably, many of the conjectures posed are
in fact false, and users often spend considerable effort examining the
theorem prover's output before realizing this. We present a
synergistic integration of testing with theorem proving, implemented
in the ACL2 Sedan (ACL2s), for automatically generating concrete
counterexamples. Our method uses the full power of the theorem prover
and associated libraries to simplify conjectures; this simplification
can transform conjectures for which finding counterexamples is hard
into conjectures where finding counterexamples is trivial. In fact, our
approach even leads to better theorem proving, e.g., if testing shows
that a generalization step leads to a false conjecture, we force the
theorem prover to backtrack, allowing it to pursue more fruitful
options that may yield a proof. The focus of the paper is on the
engineering of a synergistic integration of testing with interactive
theorem proving; this includes extending ACL2 with new functionality
that we expect to be of general interest. We also discuss our
experience in using ACL2s to teach freshman students how to reason
about their programs.

PDF (186K)