Random testing in Isabelle/HOL
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.
ps
BibTeX:
@inproceedings{Berghofer-Nipkow-SEFM2004,
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}}