2012 | OriginalPaper | Chapter
Bilateral Algorithms for Symbolic Abstraction
Authors : Aditya Thakur, Matt Elder, Thomas Reps
Published in: Static Analysis
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.