Termination Competition 2014

In 2014, the Termination Competition will be part of the FLoC Olympic Games.

Dates (tentative)

• call for solvers, certifiers, benchmarks: May 20
• registration of solvers: June 15
• updates of registered solvers, submission of benchmarks: July 1
• competition runs: July 15
• results announced: July 21, during FLoC Olympic Games Award Ceremony, Vienna.

Competition Categories and Awards

The competition contains several categories, grouped in meta-categories:

• termination of term rewriting (all categories with HO/FO-TRS, with- or without strategies)
• complexity analysis of term rewriting (all complexity categories)
• termination in programming languages (Logic Programming, Haskell, Java, C, ...)

In each meta-category, a medal will be awarded to the highest-scoring solver.

For every meta-category, we consider the sum of the scores for each category within that meta-category: The score of a tool is determined by the number of other tools which could be beaten in that category.

This puts the emphasis on categories with many competitors. (In particular, a category with just one entrant will produce zero score.)

Committees

Steering Committee

• Albert Rubio (chair), UPC Barcelona, Spain
• Frederic Mesnard, Reunion
• Jürgen Giesl, RWTH Aachen, Germany
• Johannes Waldmann, HTWK Leipzig, Germany
• Rene Thiemann, Universität Innsbruck, Austria

Organizing Commmittee

• Johannes Waldmann, HTWK Leipzig, Germany
• Stefan von der Krone, HTWK Leipzig, Germany

Technical Detail

We intend to run the competition on StarExec - a cross-community solver execution and benchmark library service under joint development (since 2012) at the University of Iowa and the University of Miami. Its goal is to facilitate the experimental evaluation of logic solvers and other automated reasoning tools by providing a shared storage and computing infrastructure to store, manage and make available benchmark libraries; execute comparative evaluations; and run solver competitions.

For displaying the results of the termination competition, we are building a separate web service at HTWK Leipzig.

Here is some information for participants:

• submit solvers for testing the platform [1]
• how to register on starexec [2] NOTE: this registration is for testing, and not for actual competition. There may be service interruptions (e.g., sudden changes in benchmark arrangement).
• STAREXEC_MAX_MEM only 750 MB? [3] (UPDATE: this was out of date, the limit is actually 64 GB)
• Beware if your solver writes to stderr. The "postprocessor" (that expects YES|NO in the first line, for termination) gets to see stdout and stderr merged. If you have trace/log output, you can only show it after the actual answer.
• hardware on starexec: see [4] Solvers are run on nodes with 4 cores each.
• software on starexec: RHEL 6.3 (so Centos 6.3 should be a close match). Package selection, see [5]
• java is available on starexec nodes (jdk 1.6.0_41) - see [6] - see also remark on ulimits and -Xmx [7]

information on the web GUI (under construction) for presenting results Star_Exec_Presenter

Separate page with impressions from using the demo version of Star Exec, in 2012: Star_Exec_Test