This paper helps to bridge the gap between (i) the use of logic for specifying program semantics and performing program analysis, and (ii) abstract interpretation. Many operations needed by an abstract interpreter can be reduced to the problem of symbolic abstraction: the symbolic abstraction of a formula φ in logic ℒ, denoted by alphaHat(φ), is the most-precise value in abstract domain A that over-approximates the meaning of φ. We present a parametric framework that, given ℒ and A, implements alphaHat. The algorithm computes successively better over-approximations of alphaHat(φ). Because it approaches alphaHat(φ) from ``above'', if it is taking too much time, a safe answer can be returned at any stage.

Moreover, the framework is``dual-use'': in addition to its applications in abstract interpretation, it provides a new way for an SMT (Satisfiability Modulo Theories) solver to perform unsatisfiability checking: given φ ∈ ℒ, the condition alphaHat(φ) = ⊥ implies that φ is unsatisfiable.

(Click here to access the paper: PDF; (c) Springer-Verlag.)