The Coq mailing list

[Stefan Berghofer <berghofe AT in.tum.de>]

Sean Wilson wrote:
> Hi,
>
> Does Coq have any facilities available to generate counter examples to 
> theorems? Specifically, I want to be able to generate counter examples to 

We have recently added such a tool (inspired by Quickcheck) to the Isabelle
theorem prover. For details, see

  Stefan Berghofer and Tobias Nipkow. Random testing in Isabelle/HOL.
  In Jorge R. Cuellar and Zhiming Liu, editors,  2nd IEEE International
  Conference on Software Engineering and Formal Methods (SEFM 2004),
  IEEE Computer Society Press 2004
  http://www4.in.tum.de/~berghofe/papers/SEFM04.pdf


Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: 
berghofe AT in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe