PostHat and All That: Automating Abstract Interpretation

Thakur, Aditya V. and Lal, Akash and Lim, Junghee and Reps, Thomas W.
Electronic Notes in Theoretical Computer Science , 2015

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     Elsevier©    

@article{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},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {311},
  pages = {15--32},
  year = {2015},
  note = {Fourth Workshop on Tools for Automatic Program Analysis (TAPAS 2013)},
  publisher = {Elsevier},
  doi = {10.1016/j.entcs.2015.02.003}
}