PostHat and All That: Automating Abstract Interpretation - Thakur, Aditya; Lal, Akash; Lim, Junghee; Reps, Thomas (The Fourth Workshop on Tools for Automatic Program Analysis (TAPAS), 2013)
Abstract interpretation provides an elegant formalism for performing program analysis. Unfortunately, designing and implementing a sound, precise, scalable, and extensible abstract interpreter is diﬃcult. In this paper, we describe an approach to creating correct-by-construction abstract interpreters that also attain the fundamental limits on precision that abstract-interpretation theory establishes. Our approach requires the analysis designer to implement only a small number of operations. In particular, we describe a systematic method for implementing an abstract interpreter that solves the following problem: Given program P, and an abstract domain A, ﬁnd the most-precise inductive A-invariant for P.