Abstract interpreters for free

Matthew Might, "Abstract interpreters for free", Static Analysis Symposium 2010 (SAS 2010).

...we present a two-step method to convert a small-step concrete semantics into a family of sound, computable abstract interpretations. The first step re-factors the concrete state-space to eliminate recursive structure; this refactoring of the state-space simultaneously determines a store-passing-style transformation on the underlying concrete semantics. The second step uses inference rules to generate an abstract state-space and a Galois connection simultaneously. The Galois connection allows the calculation of the “optimal” abstract interpretation. The two-step process is unambiguous, but nondeterministic: at each step, analysis designers face choices. Some of these choices ultimately influence properties such as flow-, field- and context-sensitivity. Thus, under the method, we can give the emergence of these properties a graph-theoretic characterization.

The work in this paper provides some context for known static analysis techniques like k-CFA, and also opens up some interesting new directions for static analysis development. Also, as Matt points out, there are some pedagogical benefits to having a systematic process for getting from semantics to abstract interpretation.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Possibly related

Supercompilation by Evaluation gives a derivation of a supercompiler from a small-step semantics. This line of research of explicitly basing transformations and analyses on the semantics seems promising.

Slightly updated version

That paper is really good and explores an interesting approach. Applying that method blindly to derive a supercompiler for a call-by-value language will not give fusion even for the most basic examples though. There's a slightly updated version of the same paper on the first author's homepage.