  Model checking invariant properties of designs, represented as transition
systems, with non-linear real arithmetic (NRA), is an important though very
hard problem. On the one hand NRA is a hard-to-solve theory; on the other hand
most of the powerful model checking techniques lack support for NRA. In this
paper, we present a counterexample-guided abstraction refinement (CEGAR)
approach that leverages linearization techniques from differential calculus to
enable the use of mature and efficient model checking algorithms for transition
systems on linear real arithmetic (LRA) with uninterpreted functions (EUF). The
results of an empirical evaluation confirm the validity and potential of this
approach.
