Theorem-Prover-Assisted Counterexample Generation With Constrained Enumerative Types

Abstract

Theorem-prover-assisted enumerative counterexample generation has been used to great effect for property-based testing in the ACL_2s theorem prover, enabling work in gamification of formal methods tasks, protocol verification, hardware verification via refinement, automated evaluation of student homework submissions and attack synthesis for distributed protocols. However, enumerative counterexample generation struggles to generate members of types under additional constraints. I present work that extends the capabilities of the existing enumerative data type framework of ACL_2s and makes it easier to integrate enumerative counterexample generation into larger systems. One approach is based on "enumerative data types modulo theories" (EDT), wherein the framework of enumerative data types used by ACL_2s is combined with constraint solvers. Another is a computational approach to handling a subset of dependent types that facilitates theorem proving while still allowing for counterexample generation. Each approach is discussed in the context of an application where it is used. I also describe several libraries that I developed that enable the implementation of EDT and its use in conjunction with systems written in other programming languages.