Show simple item record

dc.contributor.authorReps, Thomas
dc.contributor.authorLim, Junghee
dc.contributor.authorLal, Akash
dc.contributor.authorThakur, Aditya
dc.description.abstractIn abstract interpretation, the choice of an abstract domain fixes a limit on the precision of the inductive invariants that one can express; however, for a given abstract domain A, there is a most-precise (``strongest'', ``best'') inductive A-invariant for each program. Many techniques have been developed in abstract interpretation for finding over-approximate solutions, but only a few algorithms have been given that can achieve the fundamental limits that abstract-interpretation theory establishes. In this paper, we present an algorithm that solves the following problem: Given program P, an abstract domain A, and access to an SMT solver, find the most-precise inductive A-invariant for P.en
dc.subjectmachine codeen
dc.subjectpredicate abstractionen
dc.subjectsymbolic abstractionen
dc.subjectinductive invariantsen
dc.subjectabstract interpretationen
dc.titlePostHat and All That: Attaining Most-Precise Inductive Invariantsen
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