Bilateral Algorithms for Symbolic Abstraction

Given a concrete domain

$\mathcal{C}$

, a concrete operation

$\tau: \mathcal{C} \to \mathcal{C}$

, and an abstract domain

$\mathcal{A}$

, a fundamental problem in abstract interpretation is to find the

best abstract transformer

$\tau^{\#}: \mathcal{A} \to \mathcal{A}$

that over-approximates

τ

. 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

$\mathcal{L}$

, denoted by

$\widehat{\alpha}(\varphi)$

, is the best value in

$\mathcal{A}$

that over-approximates the meaning of

ϕ

. When the concrete semantics of

τ

is defined in

$\mathcal{L}$

using a formula

ϕ

τ

that specifies the relation between input and output states, the best abstract transformer

τ

#

can be computed as

$\widehat{\alpha}(\varphi_\tau)$

.

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.