| dc.contributor.author |
Thakur, Aditya |
|
| dc.contributor.author |
Reps, Thomas |
|
| dc.date.accessioned |
2012-04-06T15:31:39Z |
|
| dc.date.available |
2012-04-06T15:31:39Z |
|
| dc.date.issued |
2012-02 |
|
| dc.identifier.citation |
TR1708 |
en |
| dc.identifier.uri |
http://digital.library.wisc.edu/1793/61037 |
|
| dc.description.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. |
en |
| dc.description.provenance |
Submitted by Jason Carter (jmcarter3@wisc.edu) on 2012-04-06T15:31:39Z
No. of bitstreams: 1
tr1708.pdf: 864316 bytes, checksum: a58f0d80bf5b5541a8ca63509a8b40e6 (MD5) |
en |
| dc.description.provenance |
Made available in DSpace on 2012-04-06T15:31:39Z (GMT). No. of bitstreams: 1
tr1708.pdf: 864316 bytes, checksum: a58f0d80bf5b5541a8ca63509a8b40e6 (MD5)
Previous issue date: 2012-02 |
en |
| dc.subject |
Staalmarck's method |
en |
| dc.subject |
best transformer |
en |
| dc.subject |
symbolic abstraction |
en |
| dc.subject |
abstract interpretation |
en |
| dc.title |
A Method for Symbolic Computation of Abstract Operations |
en |
| dc.type |
Technical Report |
en |
