PostHat and All That: Attaining Most-Precise Inductive Invariants
File(s)
Date
2013-04-16Author
Reps, Thomas
Lim, Junghee
Lal, Akash
Thakur, Aditya
Metadata
Show full item recordAbstract
In 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.
Subject
machine code
predicate abstraction
symbolic abstraction
inductive invariants
abstract interpretation
Permanent Link
http://digital.library.wisc.edu/1793/65368Citation
TR1790