PostHat and All That: Attaining Most-Precise Inductive Invariants
Aditya Thakur, Akash Lal, Junghee Lim, and Thomas Reps
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:
(Click here to access the paper:
PDF.)