Existentially quantified real-algebraic formulas are Boolean combinations of constraints that compare polynomials with real-valued variables to zero. As shown by Tarski in the late 40s, real algebra allows quantifier elimination. This result implies that checking the truth of real algebraic formulas is a decidable problem, but unfortunately it is computationally hard. SMT solving attacks this problem with practically effective heuristics, separating the analysis of the Boolean structure of the formula and the consistency of the involved theory constraints.

Thus the SMT search is done by the cooperation of a SAT solver, analysing the Boolean skeleton, and a theory solver, checking the consistency of sets of theory atoms. For real-algebraic theory solvers, besides incomplete decision procedures like linearisation, interval constraint propagation, subtropical satisfiability or virtual substitution, the only complete decision procedure in use is the cylindrical algebraic decomposition (CAD) method discovered by Collins in the mid 70s which has been integrated in SMT solving.

The CAD method decomposes the state space into a finite set of disjoint regions named cells, which are arranged cylindrically in a stack-like fashion, and which have the property that all input polynomials are sign-invariant inside each of the cells. Therefore, it is sufficient to test an arbitrary point from each cell in order to determine the truth of the formula. The cells, whose shapes depend on the input polynomials and some other components used in the CAD method, build a central abstract domain for CAD.

In this invited talk we shortly introduce SMT solving and discuss relevant abstract domains for the theory of real algebra. We will put a special focus on the CAD and its cells, and illustrate how a modified abstract domain view can improve the quality of quantifier elimination.

• 2013-today: Full professor, RWTH Aachen University, Germany. Head of the research group Theory of Hybrid Systems. Research topics: SMT solving, formal methods for probabilistic and hybrid systems.

• 2008-2013: Junior professor, RWTH Aachen University, Germany. Head of the junior research group Theory of Hybrid Systems. Research topics: SMT solving, formal methods for probabilistic and hybrid systems.

• 2007-2008: Postdoctoral researcher, Jülich Research Centre, Germany. Research topics: parallel and high-performance computing, performance analysis.

• 2005-2007: Postdoctoral researcher, Albert-Ludwigs-University Freiburg, Germany. Research topics: Verification of hybrid systems, bounded model checking, SAT and SMT solving.

• 1999-2005: Ph.D. student, Christian-Albrechts-University Kiel, Germany. Research topics: Deductive proof systems for multithreaded object-oriented languages.