  We extend abstract interpretation for the purpose of verifying hybrid
systems. Abstraction has been playing an important role in many verification
methodologies for hybrid systems, but some special care is needed for
abstraction of continuous dynamics defined by ODEs. We apply Cousot and
Cousot's framework of abstract interpretation to hybrid systems, almost as it
is, by regarding continuous dynamics as an infinite iteration of infinitesimal
discrete jumps. This extension follows the recent line of work by Suenaga,
Hasuo and Sekine, where deductive verification is extended for hybrid systems
by 1) introducing a constant dt for an infinitesimal value; and 2) employing
Robinson's nonstandard analysis (NSA) to define mathematically rigorous
semantics. Our theoretical results include soundness and termination via
uniform widening operators; and our prototype implementation successfully
verifies some benchmark examples.
