PostHat and All That: Automating Abstract Interpretation
Aditya Thakur, Akash Lal, Junghee Lim, and Thomas Reps
Abstract interpretation provides an elegant formalism for performing
program analysis. Unfortunately, designing and implementing a
sound, precise, scalable, and extensible abstract interpreter is
difficult. 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:
(Click here to access the paper:
PDF.)
Given program P, and an abstract domain A,
find the most-precise inductive A-invariant for P.