A | B | C | D | E | F 
 G | H | I | J | K | L | M 
 N | O | P | Q | R | S | T 
 U | V | W | X | Y | Z 
max planck institut
informatik
mpii logo Minerva of the Max Planck Society

Homepage

Sturm, Thomas

Thomas Sturm

Email: Get my email address via email
Phone: +49 681 9325 2920
Fax: +49 681 9325 999
PGP ID: 0xD10FF471

Physical Address Mailing Address
Room 608
Campus E1 5
66123 Saarbrücken 		Max-Planck-Institut für Informatik
RG 1: Automation of Logic
Campus E1 4
66123 Saarbrücken
Germany

Research Interests

Selected Publications

  1. Verification and Synthesis Using Real Quantifier Elimination (with A. Tiwari). Proceedings of ISSAC 2011. pp.329-336, ACM Press, New York, 2011.
  2. Proceedings of the ADG 2008 (with C. Zengler, Eds.). LNCS 6301, 2011
  3. Automatic Verification of the Adequacy of Models for Families of Geometric Objects (with A. Lasaruk). Proceedings of the ADG 2008, LNCS 6301, pp.116-140, 2011.
  4. Algorithmic Global Criteria for Excluding Oscillation (with E. O. Abdel-Rahman, A. Weber). Bull. Math. Biol., 73(4):899--916, 2011.
  5. Supporting Global Numerical Optimization of Rational Functions by Generic Symbolic Convexity Tests (with W. Neun, S. Vigerske). Proceedings of the CASC 2010, LNCS 6244, pp.205-219, 2010.
  6. Parametric Quantified SAT Solving (with C. Zengler). Proceedings of the ISSAC 2010, pp.77-84. ACM Press, New York, 2010.
  7. A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra (with E. Abraham, U. Loup, F. Corzilius). 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, 2010.
  8. Effective Quantifier Elimination for Presburger Arithmetic with Infinity (with A. Lasaruk). Proceedings of the CASC 2009, LNCS 5743, pp.195-212, 2009.
  9. Investigating Algebraic and Logical Algorithms to Solve Hopf Bifurcation Problems in Algebraic Biology (with A. Weber, E. O. Abdel-Rahman, and M. El Kahoui). Math. Comput. Sci. 2(3):493-515, 2009.
  10. Investigating Generic Methods to Solve Hopf Bifurcation Problems in Algebraic Biology (with A. Weber). Proceedings of the AB 2008, LNCS 5147, pp.200-215, 2008.
  11. Redlog Online Resources for Applied Quantifier Elimination. Acta Academiae Aboensis, Ser. B, Mathematica et Physica, 67(2):177-191, 2007.
  12. Special Issue on Parametric and Nonconvex Constraint Solving (Ed. with H. Anai). Appl. Algebr. Eng. Comm., 18(6):495-496, 2007.
  13. Weak Quantifier Elimination for the Full Linear Theory of the Integers (with A. Lasaruk). Appl. Algebr. Eng. Comm., 18(6):545-574, 2007.
  14. Weak Integer Quantifier Elimination Beyond the Linear Case (with A. Lasaruk). Proceedings of the CASC 2007, LNCS 4770, pp.275-294, 2007.
  15. Special Issue on the Occasion of Volker Weispfenning's 60th Birthday (with A. Dolzmann, eds.). J. Symb. Comput., 41(11):1155-1294, 2006.
  16. New Domains for Applied Quantifier Elimination. Proceedings of the CASC 2006, LNCS 4194, pp.295-301, 2006.
  17. Quantifier Elimination for Constraint Logic Programming. Proceedings of the CASC 2005, LNCS 3718, pp.416-430, 2005.
  18. Proceedings of the A3L 2005 (with A. Dolzmann, A. Seidl, eds.). 558 p., BOD, Norderstedt, 2005.
  19. P-adic Root Isolation (with V. Weispfenning). Rev. R. Acad. Cien. Serie A. Mat. Algebra, 98(1):239-258, 2004.
  20. Solving Univariate P-adic Constraints (with V. Weispfenning). Proceedings of the CASC 2004, pp.437-449, TUM, Munich, 2004
  21. Generalized Constraint Solving over Differential Algebras (with A. Dolzmann). Proceedings of the CASC 2004, pp.111-125, TUM, Munich, 2004
  22. Efficient Projection Orders for CAD (with A. Dolzmann, A. Seidl). Proceedings of the ISSAC 2004, ACM Press, New York, 2004.
  23. Boolean Quantification in a First-Order Context (with A. Seidl). Proceedings of the CASC 2003, TUM, Müchen, 2003
  24. A Generic Projection Operator for Partial Cylindrical Algebraic Decomposition (with A. Seidl). Proceedings of the ISSAC 2003, ACM Press, New York, 2003.
  25. Quantifier Elimination in Term Algebras. The Case of Finite Languages (with V. Weispfenning). Proceedings of the CASC 2002, pp.285-300, TUM, Munich, 2002
  26. Integration of Quantifier Elimination with Constraint Logic Programming. Proceedings of the Calculemus 2002, LNAI 2385, pp.7-11, 2002. Invited paper.
  27. Parametric Systems of Linear Congruences (with A. Dolzmann). Proceedings of the CASC 2001, pp.149-166, Springer, 2001.
  28. Linear Problems in Valued Fields. J. Symb. Comput. 30(2):207-219, 2000.
  29. An Algebraic Approach to Offsetting and Blending of Solids. Proceedings of the CASC 2000, pp.367-382, Springer, 2000.
  30. Reasoning Over Networks by Symbolic Methods. Appl. Algebr. Eng. Comm., 10(1):79-96, 1999.
  31. P-adic Constraint Solving (with A. Dolzmann). Proceedings of the ISSAC 1999, pp.151-158, ACM Press, New York, 1999.
  32. Redlog User Manual. Edition 2.0 for Version 2.0 (with A. Dolzmann). Technical Report MIP-9905, FMI, Universität Passau, D-94030 Passau, Germany, April 1999.
  33. A New Approach for Automatic Theorem Proving in Real Geometry (with A. Dolzmann, V. Weispfenning). J. Autom. Reasoning 21(3):357-380, December 1998.
  34. Real Quantifier Elimination in Practice (with A. Dolzmann, V. Weispfenning). In B. H. Matzat, G.-M. Greuel, and G. Hiss, editors, Algorithmic Algebra and Number Theory, pp.221-248. Springer, 1998.
  35. Computational Geometry Problems in Redlog (with V. Weispfenning). Proceedings of the ADG 1998, LNAI 1360, pp.58-86, 1998.
  36. Approaches to Parallel Quantifier Elimination (with A. Dolzmann, O. Gloor). Proceedings of the ISSAC 1998, pp.88-95, ACM Press, New York, 1998.
  37. Redlog: Computer Algebra Meets Computer Logic (with A. Dolzmann). ACM SIGSAM Bulletin 31(2):2-9, 1997.
  38. Simplification of Quantifier-Free Formulae over Ordered Fields (with A. Dolzmann). J. Symb. Comput. 24(2):209-231, 1997.
  39. Rounding and Blending of Solids by a Real Elimination Method (with V. Weispfenning). Proceedings of the IMACS 97, pp.727-732, Wissenschaft & Technik Verlag, Berlin, 1997.
  40. Guarded Expressions in Practice (with A. Dolzmann). Proceedings of the ISSAC 97, pp.376-383, ACM Press, New York, 1997.
  41. Real Quadratic Quantifier Elimination in Risa/Asir. Research Memorandum ISIS-RM-5E, ISIS, Fujitsu Laboratories Ltd., 1-9-3, Nakase, Mihama-ku, Chiba-shi, Chiba 261, Japan, September 1996.

Teaching

Current (Winter Term 2011/2012)

Selected List of Courses / Past Teaching Activities

Recent Positions

Education

Links