PostHat and All That: Attaining Most-Precise Inductive Invariants

Abstract

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.