[Termtools] Termination competition 2011 started
Frederic Blanqui
frederic.blanqui at inria.fr
Wed Aug 17 00:18:15 CEST 2011
Hello Rene.
Would it be possible to put on the competition web page the new version
of the TPDB including the problems added in the last competition?
Thank you.
Frederic.
Le 09/06/2011 16:44, René Thiemann a écrit :
> Dear Frederic,
>
> a preliminary version of the CPFs are now available from the website. (See "Latest news / competition 2011" under http://termcomp.uibk.ac.at)
> I will officially announce it on termtools shortly, when the final version of the CPFs are available.
> The difference between the preliminary and the final version is that we plan to insert all metadata of the origin of the proof into the CPFs. This feature is not yet implemented and should be available within the next week.
>
> Cheers,
> René
>
> Am 08.06.2011 um 14:42 schrieb Frederic Blanqui:
>
>> Thank you Rene. Is there any deadline?
>>
>> Le 08/06/2011 18:38, René Thiemann a écrit :
>>> Dear Frederic,
>>>
>>> yes, of course, it is the plan to provide all CPFs. But before putting these online, I am waiting for the corrected version of AProVE-A3PAT, so that the final CPFs are linked.
>>>
>>> Concerning the coq-proofs, I just collected them and attached them in this mail (note that here still the buggy version of cime3verifier was used
>>> which transposes the matrices in the parser)
>>>
>>> Cheers,
>>> René
>>>
>>>
>>>
>>>
>>>
>>> Am 08.06.2011 um 10:05 schrieb Frederic Blanqui:
>>>
>>>
>>>> Hello Rene. I re-sent this mail to you because it was rejected by the mailing list. I don't know why. I sent a mail to Claude Marche to inform him. Frederic.
>>>>
>>>> -------- Message original --------
>>>> Sujet: Re: [Termtools] Termination competition 2011 started
>>>> Date : Wed, 08 Jun 2011 16:00:09 +0800
>>>> De : Frederic Blanqui
>>>> <frederic.blanqui at inria.fr>
>>>>
>>>> Pour :
>>>> termtools at lists.lri.fr
>>>>
>>>>
>>>>
>>>>
>>>> Hello Rene.
>>>>
>>>> Would it be possible to get a tar.gz of all the certificates (and coq
>>>> proofs?) generated in this competition?
>>>>
>>>> Thank you.
>>>>
>>>> Frederic.
>>>>
>>>> Le 30/05/2011 15:19, René Thiemann a écrit :
>>>>
>>>>> Dear all,
>>>>>
>>>>> this years international termination competition has started with 17 tools participating in 24 categories.
>>>>>
>>>>> On the first problem there is a draw between Wanda and Thor, so it will be close. However, there are around 7500
>>>>> more problems to solve.
>>>>>
>>>>> Everything can be viewed live, just visit
>>>>>
>>>>>
>>>>> http://termcomp.uibk.ac.at/
>>>>>
>>>>>
>>>>> and click on the "Live View"
>>>>>
>>>>> Enjoy and good luck to every participant,
>>>>> René
>>>>>
>
More information about the Termtools
mailing list