Integrating Testing and Interactive Theorem Proving

Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann +1

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…