Bilateral Algorithms for Symbolic Abstraction

摘要

Given a concrete domain C, a concrete operation τ : C → C, and an abstract domain A, a fundamental problem in abstract interpretation is to find the best abstract transformer τ~# : A → A that over-approximates r. This problem, as well as several other operations needed by an abstract interpreter, can be reduced to the problem of symbolic abstraction: the symbolic abstraction of a formula φ in logic (C), denoted by α(φ), is the best value in A that over-approximates the meaning of φ. When the concrete semantics of τ is defined in © using a formula φτ that specifies the relation between input and output states, the best abstract transformer τ~# can be computed as α(φτ).In this paper, we present a new framework for performing symbolic abstraction, discuss its properties, and present several instantiations for various logics and abstract domains. The key innovation is to use a bilateral successive-approximation algorithm, which maintains both an over-approximation and an under-approximation of the desired answer.