MINDS @ UW-Madison

Bilateral Algorithms for Symbolic Abstraction

Show full item record


Reps, Thomas; Elder, Matt; Thakur, Aditya
University of Wisconsin-Madison Department of Computer Sciences
Mar 28, 2012
best transformer; symbolic abstraction; abstract interpretation
Given a concrete domain C, a concrete operation tau: C -> C, and an abstract domain A, a fundamental problem in abstract interpretation is to find the best abstract transformer tau#: A -> A that over-approximates tau. This problem, as well as several other operations needed by an abstract interpreter, can be reduced to the problem of symbolic bstraction: the symbolic abstraction of a formula phi in logic L, denoted by alphaHat(phi), is the best value in A that over-approximates the meaning of phi. When the concrete semantics of tau is defined in L using a formula psi that specifies the relation between input and output states, the best abstract transformer tau# can be computed as alphaHat(psi). 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. The advantage of having a non-trivial over-approximation is that it makes the technique resilient to timeouts.
Permanent link
Export to RefWorks 

Part of

Show full item record

Search and browse


Deposit materials

  1. Register to deposit in MINDS@UW
  2. Need deposit privileges? Contact us.
  3. Already registered? Have deposit privileges? Deposit materials.