About This Item

Ask the MINDS@UW Librarian

A Method for Symbolic Computation of Abstract Operations

Show full item record

File(s):

Author(s)
Thakur, Aditya; Reps, Thomas
Citation
TR1708
Date
Feb 2012
Subject(s)
Staalmarck's method; best transformer; symbolic abstraction; abstract interpretation
Abstract
In 1979, Cousot and Cousot gave a specification of the best (most-precise) abstract transformer possible for a given concrete transformer and a given abstract domain. Unfortunately, their specification does not lead to an algorithm for obtaining the best transformer. In fact, algorithms are known for only a few abstract domains. This paper presents a parametric framework that, for a given abstract domain A and logic L, computes successively better A values that over-approximate the set of states defined by an arbitrary formula in L. Because the method approaches the most-precise A value from ``above'', if it is taking too much time, a safe answer can be returned at any time. For certain combinations of A and L, the framework is complete -- i.e., with enough resources, it computes the most-precise abstract value possible.
Permanent link
http://digital.library.wisc.edu/1793/61037 
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.