Welcome to the termination competition!

This web interface currently offers the following functionality:

  • Viewing competition results
  • Creating experiments with different termination provers
  • Registering Teams
  • Adding tools to a team and submitting implementations

More information about planned functionality and the new incarnation of the termination competition can be found in the  outline.pdf.

The current version of the TPDB, organized by categories can be downloaded here (8.0.7).

The raw version of the TPDB can be accessed via SVN: svn export http://termcomp.uibk.ac.at/svn/tpdb/trunk .

The latest set of certification problems can be downloaded here (Full run december 2013).

Latest News
Full run December 2013

The full run on TPDB 8.0.7 using recent tools is finished. Detailed results are available.

During the run, 4256 certification problems were generated.

Competition 2013

The 2013 competition was run during RTA 2013. There were 4903 challenges for termination and complexity tools of which 2314 have been solved. Moreover, 770 certification problems were generated of which all have been validated by at least one certifier (initially, there have been 6 more certification problems which turned out to be invalid proofs).

The rules of the competition and the configuration of the hardware are listed here.

The results can be viewed online via the competition result viewer where one can click on most elements to see further details.

Competition 2012

The 2012 competition was run during IJCAR 2012. There were 8077 challenges for termination and complexity tools of which 3625 have been solved. Moreover, 1264 certification problems were generated of which all have been validated by at least one certifier.

The rules of the competition and the configuration of the hardware are listed here.

The results can be viewed online via the competition result viewer where one can click on most elements to see further details.

Full run December 2011

The full run on TPDB 8 using recent tools is finished. All results are available under View competition results.

During the run, 5413 certification problems were generated.

Competition 2011

The 2011 competition was run during RTA 2011. There were 7316 challenges for termination and complexity tools of which 4110 have been solved. Moreover, 1000 certification problems were generated of which 979 have been validated by at least one certifier.

The rules of the competition and the configuration of the hardware are listed here.

The results can be viewed online via the competition result viewer where one can click on most elements to see further details.

Competition 2010

The 2010 competition was started in the morning of July 16 and was ended in the afternoon of July 20.

There have been 4232 challenges for termination and complexity tools where for 2372 problems, at least one tool was successful. Moreover, there have been 1483 certification problems of which 1454 have been validated by at least one tool. The accumulated runtime is 97 hours.

The rules of the competition and the configuration of the hardware are listed here.

Competition 2009

The results of the 2009 competition are now available. The summary overview can be found here: December 2009 summary. Also an archive of all generated proofs for certification is accessible.

Termexec Testing

A simple proof-of-concept version of termexec is now available for testing.

Read on for more detailed information.

Termcomp development

There is currently a spate of development being done on the termination competition platform. Click on read more for more information.

Jboss Richfaces by richfaces.org, version v.3.3.3.Final SVN $Revision: 16741 $ $Date: 2010-04-06 10:26:01 -0700 (Tue, 06 Apr 2010) $