Show simple item record

dc.contributor.authorReps, Thomas
dc.contributor.authorSharma, Tushar
dc.date.accessioned2017-05-16T20:55:09Z
dc.date.available2017-05-16T20:55:09Z
dc.date.issued2017-05-16T20:55:09Z
dc.identifier.citationTR1846
dc.identifier.urihttp://digital.library.wisc.edu/1793/76483
dc.description.abstractAbstract. This paper addresses the problem of abstracting a set of affine transformers v' = v C + d, where v and v' represent the pre-state and post-state, respectively. We introduce a framework to harness any base abstract domain B in an abstract domain of affine transformations. Abstract domains are usually used to define constraints on the variables of a program. In this paper, however, abstract domain B is re-purposed to constrain the elements of C and d---thereby defining a set of affine transformers on program states. This framework facilitates intra- and interprocedural analyses to obtain function and loop summaries, as well as to prove program assertions.en
dc.language.isoen_USen
dc.relation.ispartofseriestech report;TR1846
dc.subjectaffine transformersen
dc.subjectbit-vectorsen
dc.subjectprogram verificationen
dc.subjectabstract domainsen
dc.subjectabstract interpretationen
dc.titleA New Abstraction Framework for Affine Transformersen
dc.typeTechnical Reporten


Files in this item

Thumbnail
Thumbnail

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