hide
Free keywords:
-
Abstract:
The success of software verification depends on the ability to find a suitable
abstraction of a program automatically. We propose a method for automated
abstraction refinement which overcomes some limitations of current predicate
discovery schemes. In current schemes, the cause of a false alarm is identified
as an infeasible error path, and the abstraction is refined in order to remove
that path. By contrast, we view the cause of a false alarm -the spurious
counterexample- as a full-fledged program, namely, a fragment of the original
program whose control-flow graph may contain loops and represent unbounded
computations. There are two advantages to using such path programs as
counterexamples for abstraction refinement. First, we can bring the whole
machinery of program analysis to bear on path programs, which are typically
small compared to the original program. Specifically, we use constraint-based
invariant generation to automatically infer invariants of path
programs-so-called path invariants. Second, we use path invariants for
abstraction refinement in order to remove not one infeasibility at a time, but
at once all (possibly infinitely many) infeasible error computations that are
represented by a path program. Unlike previous predicate discovery schemes, our
method handles loops without unrolling them; it infers abstractions that
involve universal quantification and naturally incorporates disjunctive
reasoning.
