Abstract:

This tutorial will explore the integration of counterexample generation with interactive theorem proving, a capability that has long been on the wish list of users and developers of
interactive theorem provers.  While the generation of counterexamples is an undecidable problem, recent methods have shown that it is possible to generate counterexamples to
conjectures for many interesting problems. This tutorial will review current counterexample generation technology and how it can be used to design, analyze, and reason about systems. The tutorial will include a demo using ACL2s, the ACL2 Sedan. During the tutorial, we will also discuss the pedagogical use of counterexample generation in ACL2s to help freshmen students learn about logic and program verification. Finally, we will discuss future research opportunities.