Home > lambdatheultimate > Abstract interpreters for free

Abstract interpreters for free

August 29th, 2010 08:31 admin Leave a comment Go to comments

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.

Source: Abstract interpreters for free

Related Articles:

  1. The Galois connection between syntax and semantics
  2. Tropical Semirings
  3. Software Patents Not So Abstract When the Lawsuits Hit Home
  4. Bacteria Used To Fix Cracked Concrete
  5. Visual Hash Turns Text Or Data Into Abstract Art
blog comments powered by Disqus