[Termination tools] Rules of the WST competition

Salvador Lucas slucas at dsic.upv.es
Tue Apr 27 13:26:47 CEST 2004


Dear Claude (and all),

Claude Marche wrote:

>My idea was then that such a "competition" should be more formally
>organized so that: 
>. tools should be run all on the same computer
>. tools should be run fully automatically, as they would be run by a
>  "naive" user of the tool
>. tools should be all run on the same large set of examples.
>
I think this is a very interesting modality of testing / comparing tools 
even though
most of existing ones are not fully automatic in the previous sense (I 
mean: most
of them have many possible settings for doing the proofs which must be tuned
by the user).

>So, for this year, I will follow my first idea of running all tools on
>all the TPDB.
>
Even though there can be other suitable ways to do these comparisons, I
think interesting to do the things as you proposed. The experience will
teach us many things for sure and there will be other opportunities to try
different experiences.

Finally, I want to thank you again for all this interesting (and I think 
fruitful)
work.

Best regards,

Salvador.




More information about the Termtools mailing list