A Method for Symbolic Computation of Abstract Operations

File(s):

Author(s): Thakur, Aditya; Reps, Thomas
Citation: TR1708
Date: Feb 2012
Subject(s): Staalmarck's method; best transformer; symbolic abstraction; abstract interpretation
Abstract: In 1979, Cousot and Cousot gave a specification of the best (most-precise) abstract transformer possible for a given concrete transformer and a given abstract domain. Unfortunately, their specification does not lead to an algorithm for obtaining the best transformer. In fact, algorithms are known for only a few abstract domains. This paper presents a parametric framework that, for a given abstract domain A and logic L, computes successively better A values that over-approximate the set of states defined by an arbitrary formula in L. Because the method approaches the most-precise A value from ``above'', if it is taking too much time, a safe answer can be returned at any time. For certain combinations of A and L, the framework is complete -- i.e., with enough resources, it computes the most-precise abstract value possible.
Permanent link: http://digital.library.wisc.edu/1793/61037
Export: Export to RefWorks