Existing program analysis tools that implement abstraction rely on saturating procedures to compute over-approximations of$backslash$n fixpoints. As an alternative, we propose a new algorithm to compute an over-approximation of the set of reachable states of$backslash$n a program by replacing loops in the control flow graph by their abstract transformer. Our technique is able to generate diagnostic$backslash$n information in case of property violations, which we call leaping counterexamples. We have implemented this technique and report experimental results on a set of large ANSI-C programs using abstract domains$backslash$n that focus on properties related to string-buffers.
