[Termtools] competition

slucas at dsic.upv.es slucas at dsic.upv.es
Fri Jul 21 09:18:52 CEST 2006


Dear Claude,

Thanks for your message.

After repairing our bug and polishing our termination
expert, and since people in the list expressed some
interest on that, we have 'locally' reproduced the
competition for CSR.

You can found our results here:

    http://www.dsic.upv.es/~rgutierrez/muterm/benchmarks.html

Just 'warming the engines' for 2007 :-)

Best regards and happy summer!

Salvador.

Quoting Claude Marche <Claude.Marche at lri.fr>:

>
> On the web site
>
>   http://www.lri.fr/~marche/termination-competition/2006/
>
> you will find the report on the competition by Hans Zantema and I. In
> this report we decided to keep the results for "disqualified"
> tools. Let me quote the important sentence :
>
>   Since all tools execute complicated tasks it is likely that they
>   contain bugs. For two tools (CiME and MU-Term) we detected some
>   obviously incorrect generated proofs.  We give their results below
>   anyway, but if someone wants to use these tools, we recommend to
>   contact the authors to get a bug-fixed version.
>
> I hope this is acceptable.
>
> - Claude
>
>>>>>> "Salvador" == Salvador Lucas <slucas at dsic.upv.es> writes:
>
>     Salvador> Dear all,
>     Salvador> Zantema, H. wrote:
>
>     >> I see your problem. I agree with giving Salvador the   
> opportunity to withdraw: I can imagine that he prefers that over the  
>  situation where every one in the world can see him being   
> disqualified. I would agree with this for every disqualified tool   
> (formally or not), just like for a conference rejected papers are   
> not made public.
>     >>
>     Salvador> I also (sadly) think better to withdraw MU-TERM from   
> the 2006 competition.
>
>     >> I do not feel comfortable with the present situation where   
> Claude introduced disqualifying colors for his own tool......
>     >>
>     Salvador> Me too.
>
>     Salvador> Best regards,
>
>     Salvador> Salvador.
>
>     Salvador> _______________________________________________
>     Salvador> Termtools mailing list
>     Salvador> Termtools at lists.lri.fr
>     Salvador> http://lists.lri.fr/mailman/listinfo/termtools
>
> --
> | Claude Marché           | mailto:Claude.Marche at lri.fr |
> | LRI - Bât. 490          | http://www.lri.fr/~marche/  |
> | Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
> | F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools
>



----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.


_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools



More information about the Termtools mailing list