About This Item

Ask the MINDS@UW Librarian

A Method for Symbolic Computation

Show full item record

File(s):

Author(s)
Reps, Thomas; Thakur, Aditya
Citation
TR1702
Date
Dec 2011
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 best transformers. In fact, algorithms are known for only a few abstract domains. This paper presents a parametric framework that, for some abstract domains, is capable of obtaining best transformers in the limit. Because the method approaches best transformers from ?above?, if the computation takes too much time it can be stopped to yield a sound abstract transformer. Thus, the framework provides a tunable algorithm that offers a performance-versus-precision trade-off. We describe instantiations of the framework for well-known abstract domains, such as intervals, polyhedra, and Cartesian predicate abstraction. We also show that the framework applies to several new variants of predicate-abstraction domains that we define in the paper.
Permanent link
http://digital.library.wisc.edu/1793/60981 
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.