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