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.
Recent comments
1 hour 21 min ago
5 hours 32 min ago
18 hours 5 min ago
18 hours 8 min ago
18 hours 36 min ago
1 day 1 hour ago
1 day 1 hour ago
1 day 2 hours ago
1 day 13 hours ago
1 day 13 hours ago