Sup-interpretations, a semantic method for static analysis of program resources

Jean-Yves Marion 1 Romain Péchoux 1
1 CARTE - Theoretical adverse computations, and safety
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : The sup-interpretation method is proposed as a new tool to control memory resources of first order functional programs with pattern matching by static analysis. It has beeen introduced in order to increase the intensionality, that is the number of captured algorithms, of a previous method, the quasi-interpretations. Basically, a sup-interpretation provides an upper bound on the size of function outputs. A criterion, which can be applied to terminating as well as non-terminating programs, is developed in order to bound the stack frame size polynomially. Since this work is related to quasi-interpretation, dependency pairs and size-change principle methods, we compare these notions obtaining several results. The first result is that, given any program, we have heuristics for nding a sup-interpretation when we consider polynomials of bounded degree. Another result consists in the characterizations of the sets of functions computable in polynomial time and in polynomial space. A last result consists in applications of sup-interpretations to the dependency pair and the size-change principle methods.
Type de document :
Article dans une revue
ACM Transactions on Computational Logic, Association for Computing Machinery, 2009, 10 (4), 30 p
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00446057
Contributeur : Romain Péchoux <>
Soumis le : lundi 11 janvier 2010 - 21:58:34
Dernière modification le : mardi 18 décembre 2018 - 16:48:02
Document(s) archivé(s) le : vendredi 18 juin 2010 - 00:43:35

Fichier

333pechoux.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00446057, version 1

Collections

Citation

Jean-Yves Marion, Romain Péchoux. Sup-interpretations, a semantic method for static analysis of program resources. ACM Transactions on Computational Logic, Association for Computing Machinery, 2009, 10 (4), 30 p. 〈inria-00446057〉

Partager

Métriques

Consultations de la notice

197

Téléchargements de fichiers

126