Sciweavers

Share
SAS
2010
Springer

Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs

9 years 8 months ago
Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
Abstract. Proving the termination of a flowchart program can be done by exhibiting a ranking function, i.e., a function from the program states to a wellfounded set, which strictly decreases at each program step. A standard method to automatically generate such a function is to compute invariants for each program point and to search for a ranking in a restricted class of functions that can be handled with linear programming techniques. Previous algorithms based on affine rankings either are applicable only to simple loops (i.e., single-node flowcharts) and rely on enumeration, or are not complete in the sense that they are not guaranteed to find a ranking in the class of functions they consider, if one exists. Our first contribution is to propose an efficient algorithm to compute ranking functions: It can handle flowcharts of arbitrary structure, the class of candidate rankings it explores is larger, and our method, although greedy, is provably complete. Our second contribution is...
Christophe Alias, Alain Darte, Paul Feautrier, Lau
Added 30 Jan 2011
Updated 30 Jan 2011
Type Journal
Year 2010
Where SAS
Authors Christophe Alias, Alain Darte, Paul Feautrier, Laure Gonnord
Comments (0)
books