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}
}