Title :
Proving Program Termination by Discoverer and Complete Discrimination System
Author :
Yi Li ; Yong Feng
Author_Institution :
Automated Reasoning & Cognition Center, CIGIT, Chongqing, China
Abstract :
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.
Keywords :
polynomials; program control structures; program verification; CDS; DISCOVERER; complete discrimination system; loop program; polynomial; program termination; program verification; ranking function synthesis; DISCOVERER; complete discrimination system (CDS); invariant generation; program verification; semi-algebraic systems; termination;
Conference_Titel :
Information Science and Engineering (ISISE), 2012 International Symposium on
Conference_Location :
Shanghai
Print_ISBN :
978-1-4673-5680-0
DOI :
10.1109/ISISE.2012.15
