Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
PostHat and All That: Automating Abstract Interpretation

Aditya Thakur, Akash Lal, Junghee Lim, and Thomas Reps

Abstract

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.

Details

Publication typeInproceedings
Published inThe Fourth Workshop on Tools for Automatic Program Analysis (TAPAS)
URLhttp://research.cs.wisc.edu/wpis/abstracts/tapas13.abs.html
PublisherElsevier
> Publications > PostHat and All That: Automating Abstract Interpretation