coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Counter example generation

From: fr�d�ric BESSON <fbesson AT irisa.fr>
To: Sean Wilson <sean.wilson AT ed.ac.uk>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]Counter example generation
Date: Fri, 23 Feb 2007 10:18:17 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On 22 Feb 2007, at 13:40, Sean Wilson wrote:

Hi,

Does Coq have any facilities available to generate counter examples to
theorems?

For Coq, I am not aware of any such tool.

The only approach I am aware of is the work around Quickcheck [1] and Alfa [2].

[1] Koen Claessen John Hughes QuickCheck, A Lightweight Tool for Random Testing of Haskell Programs,
ICFP 2000

[2] Peter Dybjer, Qiao Haiyan, and Makoto Takeyama. Combining testing and proving in dependent type theory.
TPHOL 2003, volume 2758 of LNCS

Regards,

--
F. Besson

[Coq-Club]Marktoberdorf Summer School 2007 on Formal Logical Methods for System Security and Correctness, Stefan Berghofer
- [Coq-Club]Counter example generation, Sean Wilson
  - Re: [Coq-Club]Counter example generation, fr�d�ric BESSON
  - Re: [Coq-Club]Counter example generation, Stefan Berghofer
  - Re: [Coq-Club]Counter example generation, Edsko de Vries
    - Re: [Coq-Club]Counter example generation, Catherine Dubois
- <Possible follow-ups>
- [Coq-Club]Marktoberdorf Summer School 2007 on Formal Logical Methods for System Security and Correctness, Julien Narboux