Proving Program Termination by Discoverer and Complete Discrimination System

摘要

Combined with the tools DISCOVERER and CDS, a method is presented to synthesize ranking functions of loop programs. It is shown that the problems of finding ranking functions can be converted to a simpler problem, which can be solved by the complete discrimination system of polynomials (CDS), when DISCOVERER generates only one condition.