Random testing in Isabelle/HOL

Stefan Berghofer and Tobias Nipkow

When developing non-trivial formalizations in a theorem prover, a considerable amount of time is devoted to ``debugging'' specifications and conjectures by failed proof attempts. To detect such problems early in the proof and save development time, we have extended the Isabelle theorem prover with a tool for testing specifications by evaluating propositions under an assignment of random values to free variables. Distribution of the test data is optimized via mutation testing. The technical contributions are an extension of earlier work with inductive definitions and a generic method for randomly generating elements of recursive datatypes.



author={Stefan Berghofer Tobias Nipkow},
title={Random Testing in {Isabelle/HOL}},
booktitle={Software Engineering and Formal Methods (SEFM 2004)},
editor={J. Cuellar and Z. Liu},
year=2004,pages={230--239},publisher={IEEE Computer Society}}