Thomas Sturm is a CNRS research director at LORIA Nancy, France. He is also a senior researcher at Max-Planck-Institut für Informatik and a faculty member (Privatdozent) at the Department of Computer Science at Saarland University, both located in Saarbrücken, Germany.

Sturm is an editor at the Journal of Symbolic Computation (Elsevier) and at Mathematics in Computer Science (Springer).

Habilitation, Universität Passau, Germany, 2005
Dr. rer. nat., Universität Passau, Germany, 2000

Short Bio

I studied computer science at the University of Passau, Germany, where I held positions as a researcher and faculty member (Privatdozent) after finishing my studies in 1995. In 2008 I was awarded a Ramón y Cajal Fellowship by the Spanish Ministry of Science and Innovation and moved to the University of Cantabria in Santander. In 2011 I joined the MPI für Informatik in Saarbrücken, Germany, where I headed a research group for Arithmetic Reasoning. In 2016 I was appointed as a research director at CNRS.

I worked as a visiting researcher at various international institutes and research facilities including SRI International in Menlo Park, Zuse Institute Berlin, Fujitsu Laboratories Japan, Lomonosov Moscow State University, and Forschungszentrum Jülich.

Research Interests

My research interests span the domains of exact and efficient computation, computer algebra, logic, and formal reasoning. This includes the development of effective quantifier elimination methods and decision procedures for various algebraic theories, their efficient implementation, and their application in the sciences and in engineering.

One focus is interdisciplinary research on specialized decision methods for the qualitative analysis of dynamic properties of reaction systems in chemistry and systems biology.


Within the SMArT project funded by ANR and DFG I have adapted state-of-the-art arithmetic decision procedures for use within an SMT context in order to support formal system verification.

An ongoing European project SC-Square provides a platform for collaborative efforts for the communities of symbolic computation and satisfiability checking.


I have been developing the open-source computer logic system Redlog since 1992, and I am a principal developer of the open-source computer algebra system Reduce since 1995.