Abstract:
This thesis presents a counterexample generator for the interactive theorem prover Isabelle/HOL that uncovers faulty specifications and invalid conjectures using testing methods. Its contributions are two testing strategies: exhaustive testing
with concrete values; and symbolic testing, evaluating conjectures with a narrowing strategy. We present techniques to deal with conditional conjectures, including an approach to synthesize test data generators derived from the premise's definition.