Rank: a tool to check program termination and computational complexity

Christophe Alias 1 Alain Darte 1 Paul Feautrier 1 Laure Gonnord 2, 3, 4
1 COMPSYS - Compilation and embedded computing systems
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
3 LIFL - DART/Émeraude
LIFL - Laboratoire d'Informatique Fondamentale de Lille
4 DART - Contributions of the Data parallelism to real time
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
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 well-founded set that strictly decreases at each program step. In a previous paper 1 , we proposed an algorithm to compute multidimensional affine ranking functions for flowcharts of arbitrary structure. Our method, although greedy, is provably complete for the class of rankings we consider. The ranking functions we generate can also be used to get upper bounds for the computational complexity (number of transitions) of the source program. This estimate is a polynomial, which means that we can handle programs with more than linear complexity. This abstract aims at presenting R ANK, the tool that implements our algorithm.
Type de document :
Communication dans un congrès
Constraints in Software Testing Verification and Analysis, Mar 2013, Luxembourg
Liste complète des métadonnées

https://hal.inria.fr/hal-00801571
Contributeur : Laure Gonnord <>
Soumis le : dimanche 17 mars 2013 - 16:46:34
Dernière modification le : mardi 16 janvier 2018 - 15:43:17

Identifiants

  • HAL Id : hal-00801571, version 1

Collections

Citation

Christophe Alias, Alain Darte, Paul Feautrier, Laure Gonnord. Rank: a tool to check program termination and computational complexity. Constraints in Software Testing Verification and Analysis, Mar 2013, Luxembourg. 〈hal-00801571〉

Partager

Métriques

Consultations de la notice

340