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

Jan Midtgaard*, Thomas P. Jensen

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review


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. In addition to an abstract environment, the analysis computes for each expression an abstract call-stack, effectively approximating where function calls return. The analysis is systematically derived by abstract interpretation of the stack-based CaEK abstract machine of Flanagan et al. 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 transformed 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.

Original languageEnglish
JournalInformation and Computation
Pages (from-to)49-76
Number of pages28
Publication statusPublished - 1. Feb 2012


  • Abstract interpretation
  • Control-flow analysis

Fingerprint Dive into the research topics of 'Control-flow analysis of function calls and returns by abstract interpretation'. Together they form a unique fingerprint.

Cite this