A method for symbolic computation of abstract operations

Abstract

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 L, denoted by α(φ), is the most-precise value in abstract domain A that over-approximates the meaning of φ. We present a parametric framework that, given L and A, implements α. The algorithm computes successively better over-approximations of α(φ). Because it approaches α(φ) 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 φ ε L, the condition α(φ) = ⊥ implies that φ is unsatisfiable. © 2012 Springer-Verlag.