[Termtools] [color] Termination Competition 2009: Call for Participation

[Frederic Blanqui]

Dear Juergen,

could you please give more details on the way the certified category 
will be run?

 From the webpage, I can read:

"The certified categories will be run as follows:

    1. After the corresponding uncertified category of the competition 
has finished, the problems that have been solved (yes or no) are 
collected and form the initial selection for the certified category.
    2. Termination tools that can produce output in the new format and 
that participate in the certified competition are then run on the 
collection of 1, resulting in a collection of termination proofs. 
(Termination provers may use a different strategy from the uncertified 
competition, to increase chances of the proof being certified.)
    3. The certifiers are then run on the collection produced by 2."

In 3, what are the "certifiers"? Who is providing them? If there are n 
certifiers, do you mean that you are going to run the n certifiers on 
each proof provided by each tool? Finally, why do you restrict proofs to 
be in the new format (CPF I guess)? If a tool implements a new 
termination criterion and a certifier for it, it may be the case that 
there is no corresponding proof in the CPF format (yet).

Thank you for your attention.

Frederic.



Juergen Giesl a écrit :
>                   Termination Competition 2009
>                         December 16-20
> 
>                       Call for Participants
> 
> During the 90s a number of new, powerful termination methods was
> developed. Thus, at the beginning of the millennium many research
> groups started to develop tools for fully automated termination
> analysis.
> 
> After a tool demonstration at the 2003 Workshop on Termination in
> Valencia, the community decided to start an annual termination
> competition to spur the development of tools and new termination
> techniques.
> 
> The termination competition focuses on automated termination
> analysis for all kinds of programming paradigms, including
> categories for term rewriting, logic programming, functional
> programming, and imperative programming. It serves to demonstrate
> the power of the leading tools in each of these areas.
> 
> At the 2009 Workshop on Termination in Leipzig, the community
> decided to move to an online execution. In every category,
> all participating tools of that category are run
> on a randomly selected subset of the available problems.
> 
> This new approach will be followed in the 2009 competition as well as
> in the next live competition at FLoC 2010. Additionally, in this
> competition a new category on Java bytecode programs will start.
> 
> Details about the new rules, machine configuration, etc. can be found
> at
> 
>   http://termcomp.uibk.ac.at/status/rules.html
> 
> Due to the significant changes introduced in the competition and with
> the aim of extracting as much knowledge as possible about the new
> execution system and the new rules that will be used from now on in
> the termination competition, we strongly encourage all developers of
> termination tools to participate in the competition. Moreover, tools
> are also encouraged to participate in as much categories of the competition
> as possible.
> 
> Moreover, if there is no category that is convenient for your tool, you
> can contact the organizers, since other categories can be considered
> as well (this year or in 2010) if enough participants are guaranteed.
> 
> Important dates
> 
> Problem submission:   2 December 2009,   23:59 CET (Wednesday midnight)
> 
> Software requests:    2 December 2009,   23:59 CET (Wednesday midnight)
> 
> Tool submission:     14 December 2009,   12:01 CET (Monday midday)
> 
> Competition start:   16 December 2009,   12:01 CET (Wednesday midday)