Show simple item record

dc.contributor.authorReps, Thomas
dc.contributor.authorThakur, Aditya
dc.contributor.authorSharma, Tushar
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


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