Show simple item record

dc.contributor.authorThakur, Aditya
dc.contributor.authorReps, Thomas
dc.description.abstractIn 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.subjectStaalmarck's methoden
dc.subjectbest transformeren
dc.subjectsymbolic abstractionen
dc.subjectabstract interpretationen
dc.titleA Method for Symbolic Computation of Abstract Operationsen
dc.typeTechnical Reporten

Files in this item


This item appears in the following Collection(s)

  • CS Technical Reports
    Technical Reports Archive for the Department of Computer Sciences at the University of Wisconsin-Madison

Show simple item record