Leaping loops in the presence of abstraction
============================================

Finite abstraction helps program analysis cope with the huge state
space of programs. We wish to use abstraction in the process of error
detection. Such a detection involves reachability analysis of the
program. Reachability in an abstraction that under-approximates the
program implies reachability in the concrete system.
Under-approximation techniques, however, lose precision in the
presence of loops, and cannot detect their termination. This causes
reachability analysis that is done with respect to an abstraction to
miss states of the program that are reachable via loops.  Current
solutions to this loop-termination challenge are based on fair
termination and involve the use of well-founded sets and ranking
functions.

In many cases, the concrete system has a huge, but still finite set of
states. Our contribution is to show how, in such cases, it is possible
to analyze termination of loops without refinement and without
well-founded sets and ranking functions. Instead, our method is based
on conditions on the structure of the graph that corresponds to the
concrete system --- conditions that can be checked with respect to the
abstraction. We describe our method, demonstrate its usefulness and
show how its application can be automated by means of a theorem
prover.