  We present two characterizations of positive invariance of sets under the
flow of systems of ordinary differential equations. The first characterization
uses inward sets which intuitively collect those points from which the flow
evolves within the set for a short period of time, whereas the second
characterization uses the notion of exit sets, which intuitively collect those
points from which the flow immediately leaves the set. Our proofs emphasize the
use of the real induction principle as a generic and unifying proof technique
that captures the essence of the formal reasoning justifying our results and
provides cleaner alternative proofs of known results. The two characterizations
presented in this article, while essentially equivalent, lead to two rather
different decision procedures (termed respectively LZZ and ESE) for checking
whether a given semi-algebraic set is positively invariant under the flow of a
system of polynomial ordinary differential equations. The procedure LZZ
improves upon the original work by Liu, Zhan and Zhao (EMSOFT 2011). The
procedure ESE, introduced in this article, works by splitting the problem, in a
principled way, into simpler sub-problems that are easier to check, and is
shown to exhibit substantially better performance compared to LZZ on problems
featuring semi-algebraic sets described by formulas with non-trivial Boolean
structure.
