Certified Termination

From Termination-Portal.org
Jump to navigationJump to search

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: