News

Termination Competition 2010   (20 July, 2010)

The 6th international competition of termination tools is over. Three termination tools and one certifier, developed at our group, participated and all of them won in at least one of several categories.

Proving termination of programs (automatically) is a challenging endeavour since for most programming languages the property of termination is undecidable. Nevertheless by now there are automatic tools that can prove (non)termination of a large class of programs.

The international competition of termination tools is executed annually since 2004, after a tool demonstration in 2003. Since 2007 a certified category is installed, where it is required that the termination tools produce output that is then verified by means of a theorem prover. In 2008 special categories for proving upper bounds on the complexity of programs were started. From 2004 to 2007 the competition was hosted in Paris and from 2008 on the computational logic group from the university of Innsbruck organises the contest.

In 2010 there have been 23 categories and tools from Innsbruck participated in 12 of them, 5 of which they won. All these tools are open source.

  • CaT was the strongest tool for derivational complexity
  • CeTA was the most powerful certifier (in all 4 certifying categories)
  • TCT2 won the innermost derivational complexity and runtime complexity categories
  • TTT2 won the standard SRS (draw with AProVE) and standard SRS certifying categories

Links: