Difference between revisions of "Certified Termination"
From Termination-Portal.org
Jump to navigationJump to searchJ.waldmann (talk | contribs) (Created page with '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 prob…') |
|||
| Line 9: | Line 9: | ||
* [[WScT|Workshops on Certified Termination]] | * [[WScT|Workshops on Certified Termination]] | ||
* unified format for (non-)termination certificates: http://cl-informatik.uibk.ac.at/software/cpf/ | * unified format for (non-)termination certificates: http://cl-informatik.uibk.ac.at/software/cpf/ | ||
| + | |||
| + | [[Category:Categories]] | ||
Latest revision as of 14:40, 21 December 2009
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/
