[PL Seminar] Talk: Jan Midtgaard

Title:
A Calculational Approach to Control-flow Analysis by Abstract Interpretation

Speaker:
Jan Midtgaard
IRISA / INRIA Rennes - Bretagne Atlantique

Abstract:
We present a derivation of a control-flow analysis by abstract
interpretation. Our starting point is a transition system semantics
defined as an abstract machine for a small functional language in
continuation-passing style. We obtain a Galois connection for
abstracting the machine states by composing Galois connections, most
notable an independent-attribute Galois connection on machine states and
a Galois connection induced by a closure operator associated with a
constituent-parts relation on environments. We calculate abstract
transfer functions by applying the state abstraction to the collecting
semantics, resulting in a demand-driven 0-CFA. We thereby provide a
novel characterization of the analysis.

Joint work with Thomas Jensen

Biosketch:
Jan Midtgaard is post-doctoral researcher at IRISA / INRIA Rennes. He
received a PhD in computer science from BRICS, Department of Computer
Science at the University of Aarhus in 2007. His education included
notable visits to Harvard University and Ecole Normale Supérieure in
Paris. Jan's research interests include program analysis and
transformation, programming language implementation and semantics - and
the combinations hereof.

Host: Olivier Danvy