Bilateral Algorithms for Symbolic Abstraction

Thakur, Aditya V. and Elder, Matt and Reps, Thomas W.
19th International Symposium on Static Analysis (SAS), 2012

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 τ. 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 L, denoted by alphaHat(φ), is the best value in A that over-approximates the meaning of φ. When the concrete semantics of τ is defined in L using a formula ψ that specifies the relation between input and output states, the best abstract transformer τ# can be computed as alphaHat(ψ).

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.

PDF     Springer©    

@inproceedings{thakur_etal_SAS12,
  author = {Thakur, Aditya V. and Elder, Matt and Reps, Thomas W.},
  title = {Bilateral Algorithms for Symbolic Abstraction},
  booktitle = {19th International Symposium on Static Analysis ({SAS})},
  year = {2012},
  pages = {111--128},
  publisher = {Springer},
  doi = {10.1007/978-3-642-33125-1_10}
}