[Termination tools] announcement termination competition

[Juergen Giesl]

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