Skip to Main content Skip to Navigation
New interface
Journal articles

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.
Document type :
Journal articles
Complete list of metadata

Cited literature [43 references]  Display  Hide  Download
Contributor : Thomas Jensen Connect in order to contact the contributor
Submitted on : Thursday, November 29, 2012 - 1:22:59 PM
Last modification on : Thursday, January 20, 2022 - 5:33:19 PM
Long-term archiving on: : Saturday, December 17, 2016 - 4:10:39 PM


Files produced by the author(s)



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



Record views


Files downloads