Automatic Discovery of Non-Ranking Functions with DISCOVERER
Lin Mu, Xiao Dong Qiao, Chun Yun Hao, Yong Xiang Mu · Applied Mechanics and Materials · 2013
This paper proposes a definition of non-ranking functions of loop programs and investigates how to apply the techniques on synthesize Non-ranking functions of loop programs. It is shown that this new non-ranking function works well to determine the termination of loop programs.