Control-flow analysis of function calls and returns by abstract interpretation

Jan Midtgaard 1 Thomas Jensen 2
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Abstract interpretation techniques are used to derive a control-flow analysis for a simple higher-order functional language. The analysis approximates the interprocedural control-flow of both function calls and returns in the presence of first-class functions and tail-call optimization. The analysis is systematically derived by abstract interpretation of a stack-based abstract machine using a series of Galois connections. We prove that the analysis is equivalent to an analysis obtained by first transforming the program into continuation-passing style and then performing control flow analysis of the transfored program. We then show how the analysis induces an equivalent constraint-based formulation, thereby providing a rational reconstruction of a constraint-based CFA from abstract interpretation principles.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2012, 2012, pp.49-76. <10.1016/j.ic.2011.11.005>
Liste complète des métadonnées


https://hal.inria.fr/hal-00758152
Contributeur : Thomas Jensen <>
Soumis le : jeudi 29 novembre 2012 - 13:22:59
Dernière modification le : mercredi 2 août 2017 - 10:11:34
Document(s) archivé(s) le : samedi 17 décembre 2016 - 16:10:39

Fichier

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

Identifiants

Citation

Jan Midtgaard, Thomas Jensen. Control-flow analysis of function calls and returns by abstract interpretation. Information and Computation, Elsevier, 2012, 2012, pp.49-76. <10.1016/j.ic.2011.11.005>. <hal-00758152>

Partager

Métriques

Consultations de
la notice

810

Téléchargements du document

130