[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