  In this work, we consider the fundamental problem of reachability analysis
over imperative programs with real variables. The reachability property
requires that a program can reach certain target states during its execution.
Previous works that tackle reachability analysis are either unable to handle
programs consisting of general loops (e.g. symbolic execution), or lack
completeness guarantees (e.g. abstract interpretation), or are not automated
(e.g. incorrectness logic/reverse Hoare logic). In contrast, we propose a novel
approach for reachability analysis that can handle general programs, is
(semi-)complete, and can be entirely automated for a wide family of programs.
Our approach extends techniques from both invariant generation and
ranking-function synthesis to reachability analysis through the notion of
(Universal) Inductive Reachability Witnesses (IRWs/UIRWs). While traditional
invariant generation uses over-approximations of reachable states, we consider
the natural dual problem of under-approximating the set of program states that
can reach a target state. We then apply an argument similar to ranking
functions to ensure that all states in our under-approximation can indeed reach
the target set in finitely many steps.
