Counterexample Generation for Higher-Order Logic Using Functional and Logic Programming
Lukas Bulwahn · mediaTUM – the media and publications repository of the Technical University Munich (Technical University Munich) · 2013
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.