[Termination tools] announcement termination competition

[Salvador Lucas]

Dear all,

I mostly agree with Juergen.

Of course, time is an important issue
for any software analysis tool.

However, in our setting I think it
should not be the most important thing.

On my side, I would prefer to concentrate
in implementing new techniques to test
their applicability in termination proofs
rather than trying to improve MU-TERM to
become a very fast tool. This is my main
motivation to join the 'competition'...

If we set a very low time limit, then the
possible application of new techniques and
developments could become just unnoticed.
I do not think this is so good.

On the other hand, fast tools will shine
anyway if (as expected) appropriate
information abou the amount of time
spent to solve the problems is given.

Best regards,

Salvador.

Juergen Giesl wrote:

> Dear Claude and Hans,
>
>
> also, thank you very much for taking up the work
> and organizing the termination competition.
>
> Concerning Aart's suggestion:
>
>
>>> * There should be a fixed time limit for each termination problem. It
>>>   is proposed to define it to be one minute. 
>>
>>
>>
>> I propose in addition to have a very short time limit
>> (e.g. 1 second), in order to stimulate the quest for
>> fast implementations of basic techniques as well as the
>> development of efficient automatic strategies. With only
>> a one minute time limit, it is very tempting to incorporate
>> as many techniques as possible into one system. For the
>> same reasons I think it make sense to keep systems in the
>> competition that were solved by all systems last year; the
>> difference in the employed techniques by the participating
>> systems is interesting as is any time difference between
>> different implementations of the same technique.
>
>
> I disagree with this suggestion, since the amount of time
> needed also depends a lot on the programming language used.
> Then the competition would mainly show the differences in speed
> between different programming languages, but not the differences
> between the different algorithms used for proving termination.
>
> (In particular, in the setting of the competition, the systems
> are started again on every new example. Since the
> the start-up time of Java and the JVM is more
> than 1 second, AProVE would not be able to prove any example
> within 1 second in this setting. Hence, it would make no sense for
> us to participate in the competition anymore.)
>
> Clearly, there has to be some time limit to run the competition
> in finite time. I think that your proposal of 1 minute (the
> same as last year) is fine.
>
> Best Regards
> Juergen
>
>
>
>