Using bounded model checking to focus fixpoint iterations

Two classical sources of imprecision in static analysis by abstract inter-pretation are widening and merge operations. Merge operations can be done away by distinguishing paths, as in trace partitioning, at the expense of enu-merating an exponential number of paths. In this article, we describe how to avoid such systematic exploration by focusing on a single path at a time, designated by SMT-solving. Our method combines well with acceleration techniques, thus doing away with widenings as well in some cases. We illustrate it over the well-known domain of convex polyhedra.