PostHat and all that: Automating abstract interpretation

Thakur, Aditya V. and Lal, Akash and Lim, Junghee and Reps, Thomas W.
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 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:

Given program P, and an abstract domain A, find the most-precise inductive A-invariant for P.

PDF    

@inproceedings{thakur_etal_TAPAS13,
  author = {Thakur, Aditya V. and Lal, Akash and Lim, Junghee and Reps, Thomas W.},
  title = {PostHat and all that: Automating abstract interpretation},
  booktitle = {Fourth Workshop on Tools for Automatic Program Analysis (TAPAS)},
  publisher = {Electronic Notes Theoretical Computer Science},
  year = {2013}
}