Show simple item record

dc.contributor.authorReps, Thomas
dc.contributor.authorLim, Junghee
dc.contributor.authorLal, Akash
dc.contributor.authorThakur, Aditya
dc.date.accessioned2013-04-18T15:09:25Z
dc.date.available2013-04-18T15:09:25Z
dc.date.issued2013-04-16
dc.identifier.citationTR1790en
dc.identifier.urihttp://digital.library.wisc.edu/1793/65368
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

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