Show simple item record

dc.contributor.authorReps, Thomas
dc.contributor.authorThakur, Aditya
dc.contributor.authorSharma, Tushar
dc.date.accessioned2013-04-18T15:02:19Z
dc.date.available2013-04-18T15:02:19Z
dc.date.issued2013-04-16
dc.identifier.citationTR1789en
dc.identifier.urihttp://digital.library.wisc.edu/1793/65366
dc.description.abstractThis paper advances the state of the art in abstract interpretation of machine code. It tackles two of the biggest challenges in machine-code analysis: (1) holding onto invariants about values in memory, and (2) identifying affine-inequality invariants while handling overflow in arithmetic operations over bit-vector data-types. Most current approaches either capture relations only among registers (and ignore memory entirely), or make potentially unsound assumptions when handling memory. Furthermore, existing bit-vector domains are able to represent either relational affine equalities or non-relational inequalities (e.g., intervals). The key insight to tackling both challenges is to define a new domain combinator (denoted by V), called the view-product combinator. V constructs a reduced product of two domains in which shared view-variables are used to communicate information among the domains. V applied to a non-relational memory domain and a relational bit-vector affine-equality domain constructs the Bit-Vector Memory-Equality Domain (BVME), a domain of bit-vector affine-equalities over memory and registers. V applied to the BVME domain and a bit-vector interval domain constructs the Bit-Vector Memory-Inequality Domain, a domain of relational bit-vector affine-inequalities over memory and registers.en
dc.publisherUniversity of Wisconsin-Madison Department of Computer Sciences
dc.subjectmodular arithmeticen
dc.subjectsymbolic abstractionen
dc.subjectdomain combinationen
dc.subjectmachine codeen
dc.subjectabstract interpretationen
dc.titleAn Abstract Domain for Bit-Vector Inequalitiesen
dc.typeTechnical Reporten


Files in this item

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