Title :
Automated verification of loops with assignments only by recurrence solving and optimization problems
Author :
Xing, Jianying ; Li, Mengjun ; Li, Zhoujun
Author_Institution :
Sch. of Comput. Sci., Nat. Univ. of Defense Technol., Changsha, China
Abstract :
Based on techniques of solving recurrence equations and optimization problems, we present a practical approach for verifying program including loops with assignments only. We implement this approach on the platform of Mathmatica. The experimental results demonstrate the power of our approach.
Keywords :
optimisation; program control structures; program verification; Mathmatica; automated loops verification; optimization problems; program verification; recurrence equation solving; Arithmetic; Computer languages; Computer science; Difference equations; Formal verification; Logic; Polynomials; Power engineering and energy; Safety; Surface-mount technology; optimization problem; program verification; recurrence equations; termination;
Conference_Titel :
Future Computer and Communication (ICFCC), 2010 2nd International Conference on
Conference_Location :
Wuhan
Print_ISBN :
978-1-4244-5821-9
DOI :
10.1109/ICFCC.2010.5497670
