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...

• Type: Journal
• Year: 2010
• Where: SAS
• Authors: Christophe Alias, Alain Darte, Paul Feautrier, Laure Gonnord
• Keywords: Formal Methods, Linear Programming Techniques, Ranking, Ranking Functions, SAS 2010