Certified Termination

From the rules of the 2009 competition: The certified categories will be run as follows:

• 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.
• 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.)
• The certifiers are then run on the collection produced by 2.

see also:

• Workshops on Certified Termination
• unified format for (non-)termination certificates: http://cl-informatik.uibk.ac.at/software/cpf/