Theory and Practice of Control-Flow Analysis of Higher Order Languages by Systematic Abstraction of Abstract Machines

March 12, 2013

Ilya Sergey


Theory and Practice of Control-Flow Analysis of Higher Order Languages by Systematic Abstraction of Abstract Machines

Time:   11:00am
Location:   Meeting room 302 (Mountain View), level 3

In this informal two-part talk I will present recent studies on systematic construction of control-flow analyses for higher-order languages by means of abstract interpretation. In the first part of the talk, I will give a tutorial on turning a small-step abstract machine into an abstract interpreter, delivering the flows-to information by approximating collecting semantics of a program. The key idea of the approach is eliminating circular dependencies in a semantic state-space and then bounding it by providing an abstraction over its leaf elements. I will also briefly describe advanced techniques, allowing one to improve precision and complexity boundaries of the analysis: widening, abstract garbage collection and counting. The second part of the talk is more of implementation flavour. Following the same story line, I show a systematic method for transforming a concrete semantics into a monadically-parameterized abstract machine, such that changing the monad changes the behaviour of the machine. By changing the monad, we can recover a spectrum of machines - from the original concrete semantics to a monovariant, flow- and context-insensitive static analysis with a singly-threaded heap and weak updates. The monadic parameterization also suggests an abstraction over the ubiquitous monotone fixed-point computation found in static analysis. This abstraction makes it straightforward to instrument an analysis with high-level strategies for improving precision and performance, such as abstract garbage collection and widening.