About This Item

Ask the MINDS@UW Librarian

Bilateral Algorithms for Symbolic Abstraction

Show full item record

File(s):

Author(s)
Reps, Thomas; Elder, Matt; Thakur, Aditya
Publisher
University of Wisconsin-Madison Department of Computer Sciences
Citation
TR1713
Date
Mar 28, 2012
Subject(s)
best transformer; symbolic abstraction; abstract interpretation
Abstract
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
http://digital.library.wisc.edu/1793/60977 
Export
Export to RefWorks 
‚Äč

Part of

Show full item record

Search and browse




About MINDS@UW

Deposit materials

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