There are several methods for the synthesis and analysis of hybrid

systems that require efficient algorithms and tools for satisfiability

checking. For analysis, e.g., bounded model checking describes

counterexamples of a fixed length by logical formulas, whose

satisfiability corresponds to the existence of such a counterexample.

As an example for parameter synthesis, we can state the correctness of

a parameterized system by a logical formula; the solution set of

the formula gives us possible safe instances of the parameters.

For discrete systems, which can be described by propositional logic

formulas, SAT-solvers can be used for the satisfiability checks. For

hybrid systems, having mixed discrete-continuous behavior, SMT-solvers

are needed. SMT-solving extends SAT with theories, and has its main

focus on linear arithmetic, which is sufficient to handle, e.g.,

linear hybrid systems. However, there are only few solvers for

more expressive but still decidable logics like the

first-order theory of the reals with addition and multiplication --

real algebra. Since the synthesis and analysis of non-linear

hybrid systems requires such a powerful logic, we need efficient

SMT-solvers for real algebra. Our goal is to develop such an

SMT-solver for the real algebra, which is both complete and

efficient.