Applications in Verification

  1. Ton-Chanh Le, Cristian Gherghina, Razvan Voicu, Wei-Ngan Chin. A Proof Slicing Framework for Program Verification. ICFEM 2013
  2. Jan-David Quesel. Similarity, Logic, and Games: Bridging Modeling Layers of Hybrid Systems. Report 03-13, Department for Informatics, University of Oldenburg, Germany, 2013
  3. Roberto Bagnara, Fred Mesnard. Eventual Linear Ranking Functions. CoRR, abs/1306.1901, 2013
  4. Sriram Sankaranarayanan, Ashish Tiwari. Relational Abstractions for Continuous and Hybrid Systems. CAV 2011, LNCS 6806, pp.686–702, 2011
  5. Werner Damm, Carsten Ihlemann, Viorica Sofronie-Stokkermans. Decidability and Complexity for the Verification of Safety Properties of Reasonable Linear Hybrid Automata. HSCC 2011, pp.73–82, ACM Press, 2011
  6. Thomas Sturm, Ashish Tiwari. Verification and Synthesis Using Real Quantifier Elimination. ISSAC 2011, pp.329–336, ACM Press, 2011
  7. Joost-Pieter Katoen, Annabelle K. McIver, Larissa A. Meinicke, Carroll C. Morgan. Linear-invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods. SAS 2010, LNCS 6337, pp.390–406, 2010
  8. André Platzer, Jan-David Quesel, Philipp Rümmer. Real World Verification. CADE 2009, LNCS 5663, pages 485–501, 2009
  9. Viorica Sofronie-Stokkermans. Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions. FroCoS 2007, LNAI 4720, pp.47–71, 2007
  10. Hugh Anderson, Siau-Cheng Khoo, Stefan Andrei, Beatrice Luca. Calculating Polynomial Runtime Properties. APLAS 2005, LNCS 3780, pp.230–245, 2005
  11. Michael Colón, Sriram Sankaranarayanan, Henny Sipma. Linear Invariant Generation Using Non-Linear Constraint Solving. CAV 2003, LNCS 2725, pp.420–432, 2003
  12. Hirokazu Anai, Volker Weispfenning. Reach Set Computations Using Real Quantifier Elimination. HSCC 2001, LNCS 2034, 2001
  13. Gerardo Lafferriere, George J. Pappas, Sergio Yovine. Symbolic Reachability Computation for Families of Linear Vector Fields. J. Symb. Comput. 32(3):231-253, 2001
  14. Aurore Annichini, Ahmed Bouajjani, Mihaela Sighireanu. TReX: A Tool for Reachability Analysis of Complex Systems. CAV 2001, LNCS 2102, pp.368–372, 2001

Applications in Chemistry and the Life Sciences

  1. Hassan Errami, Markus Eiswirth, Dimar Grigoriev, Werner Seiler, Thomas Sturm, Andreas Weber. Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates. CASC 2013, to appear in LNCS
  2. Alberto Casagrande, Tommaso Dreossi, Carla Piazza. Hybrid Automata and ε-Analysis on a Neural Oscillator. HSB 2012, EPTCS 92, pp.58–72, 2012
  3. Hassan Errami, Thomas Sturm, Andras Weber. Algorithmic Aspects of Muldowney's Extension of the Bendixson-Dulac Criterion for Polynomial Vector Fields. Polynomial Computer Algebra, pp.25–28, Euler Institute, Petersburg, 2011
  4. Essam Abdel-Rahman, Thomas Sturm, Andreas Weber. Algorithmic Global Criteria for Excluding Oscillation. Bull. Math. Biol., 73(4):899–916, 2011
  5. Andreas Weber, Essam O. Abdel-Rahman, M'hammed El Kahoui, Thomas Sturm. Investigating Algebraic and Logical Algorithms to Solve Hopf Bifurcation Problems in Algebraic Biology. Math. Comput. Sci. 2(3):493–515, 2009
  6. Thomas Sturm, Andreas Weber. Investigating Generic Methods to Solve Hopf Bifurcation Problems in Algebraic Biology. AB 2008, LNCS 5147, pp.200–215, 2008
  7. Christopher W. Brown, M'hammed El Kahoui, Dominik Novotni, Andreas Weber. Algorithmic Methods for Investigating Equilibria in Epidemic Modeling. J. Symb. Comput. 41(11):1157-1173, 2006
  8. Werner M. Seiler, Andreas Weber. Deciding Ellipticity by Quantifier Elimination. CASC 2004, pp.347–355, TU München, 2003
  9. M'hammed Kahoui, Andreas Weber. Symbolic Equilibrium Point Analysis in Parameterized Polynomial Vector Fields. CASC 2002, pp.71–83, TU München, 2002
  10. M'hammed Kahoui, Andreas Weber. Deciding Hopf Bifurcations by Quantifier Elimination in a Software Component Architecture. J. Symb. Comput. 30(2):161-179, 2000

Applications in Physics and Engineering

  1. Thomas Sturm. Reasoning over Networks by Symbolic Methods. Appl. Algebr. Eng. Comm. 10(1):79-96, 1999
  2. Nikolaos I. Ioakimidis. Finite Differences/Elements in Classical Beam Problems: Derivation of Feasibility Conditions Under Parametric Inequality Constraints with the Help of Reduce and Redlog. Computational Mechanics, 27(2):145-153, 2001
  3. Nikolaos I. Ioakimidis. Automatic Derivation of Positivity Conditions Inside Boundary Elements with the Help of the Redlog Computer Logic Package. Engineering Analysis with Boundary Elements 23(10):847-856, 1999
  4. Nikolaos I. Ioakimidis. Redlog-Aided Derivation of Feasibility Conditions in Applied Mechanics and Engineering Problems Under Simple Inequality Constraints. Journal of Mechanical Engineering (Strojnicky Casopis) 50(1):58-69, 1999

Applications in Scientific Computation

  1. Hidenao Iwane, Hitoshi Yanami, Hirokazu Anai. A Symbolic-Approach to Multi-Objective Optimization in Manufacturing Design. Math. Comput. Sci. 5(3)315–334, 2011
  2. Winfried Neun, Thomas Sturm, Stefan Vigerske. Supporting Global Numerical Optimization of Rational Functions by Generic Symbolic Convexity Tests. CASC 2010, LNCS 6244, pp.205–219, 2010
  3. Andreas Dolzmann, Thomas Sturm. Parametric Systems of Linear Congruences. CASC 2001, pp.149–166, Springer, 2001
  4. Andreas Dolzmann. Solving Scheduling Problems with Redlog. RWCA 1998, extended abstract, 1998
  5. Volker Weispfenning. Simulation and Optimization by Quantifier Elimination. J. Symb. Comput. 24(2):189-208, 1997

Applications in Geometry and Planning

  1. Aless Lasaruk, Thomas Sturm. Automatic Verification of the Adequacy of Models for Families of Geometric Objects. ADG 2008, LNCS 6301, pp.116–140, 2011
  2. Thomas Sturm. An Algebraic Approach to Offsetting and Blending of Solids. CASC 2000, pp.367–382, Springer, 2000
  3. Volker Weispfenning. Semilinear Motion Planning in Redlog. Appl. Algebr. Eng. Comm. 12:455-475, 2001
  4. Andreas Dolzmann. Solving Geometric Problems with Real Quantifier Elimination. Technical Report MIP-9903, Universität Passau, 1999
  5. Thomas Sturm, Volker Weispfenning. Computational Geometry Problems in Redlog. ADG 1998, LNAI 1360, pp.58–86, 1998
  6. Andreas Dolzmann, Thomas Sturm, Volker Weispfenning. A New Approach for Automatic Theorem Proving in Real Geometry. J. Autom. Reasoning 21(3):357–380, 1998
  7. Thomas Sturm, Volker Weispfenning. Rounding and Blending of Solids by a Real Elimination Method. IMACS 1997, pp.727–732, Wissenschaft & Technik Verlag, Berlin, 1997

Other Applications

  1. Thomas Sturm. Quantifier Elimination for Constraint Logic Programming. CASC 2005, LNCS 3718, pp.416–430, 2005
  2. Thomas Sturm. Integration of Quantifier Elimination with Constraint Logic Programming. Calculemus 2002, LNAI 2385, pp.7–11, 2002
  3. Andreas Dolzmann, Thomas Sturm, Volker Weispfenning. Real Quantifier Elimination in Practice. Algorithmic Algebra and Number Theory, pp.221–248. Springer, 1998
  4. Guarded Expressions in Practice. ISSAC 1997, pp.376–383, ACM Press, 1997

Nonlinear Real Arithmetic in Redlog

  1. Andreas Dolzmann, Andreas Seidl, Thomas Sturm. Efficient Projection Orders for CAD. ISSAC 2004, ACM Press, 2004
  2. Andreas Seidl, Thomas Sturm. A Generic Projection Operator for Partial Cylindrical Algebraic Decomposition. ISSAC 2003, ACM Press, 2003
  3. Andreas Dolzmann, Volker Weispfenning. Local Quantifier Elimination. ISSAC 2000, ACM Press, 2000
  4. Andreas Dolzmann, Oliver Gloor, Thomas Sturm. Approaches to Parallel Quantifier Elimination. ISSAC 1998, ACM Press, 1998
  5. Andreas Dolzmann, Thomas Sturm. Simplification of Quantifier-free Formulae over Ordered Fields. J. Symb. Comput. 24(2):209-231, 1997

Integer Arithmetic in Redlog

  1. Aless Lasaruk, Thomas Sturm. Weak Quantifier Elimination for the Full Linear Theory of the Integers
    Appl. Algebr. Eng. Comm. 18(6):545–574, 2007
  2. Aless Lasaruk, Thomas Sturm. Weak Integer Quantifier Elimination Beyond the Linear Case. CASC 2007, LNCS 4770, pp.275–294, 2007

Parametric QSAT in Redlog

  1. T. Sturm, C. Zengler. Parametric Quantified SAT Solving. ISSAC 2010, pp.77–84. ACM Press, 2010
  2. Andreas Seidl, Thomas Sturm. Boolean Quantification in a First-Order Context. CASC 2003, TU München, 2003

Other Theories Supported by Redlog

  1. Christian Straßer. Quantifier Elimination for Queues. RWCA 2006, pp.239–248, Universität Basel, 2006
  2. Christian Straßer. Quantorenelimination von Queues. Diploma Thesis. Universität Passau, 2006 (in German)
  3. Christian Hoffelner. Quantifier Elimination-based Parametric Solving in Term Algebras. Diploma Thesis. Universität Passau, 2005
  4. Thomas Sturm, Volker Weispfenning. Quantifier Elimination in Term Algebras. The Case of Finite Languages. CASC 2002, pp.285–300, TU München, 2002
  5. Andreas Dolzmann, Thomas Sturm. Generalized Constraint Solving over Differential Algebras. CASC 2004, pp.111–125, TU München, 2004
  6. Andreas Dolzmann, Thomas Sturm. P-adic Constraint Solving. ISSAC 1999, ACM Press, 1999

Other Redlog Papers

  1. Thomas Sturm. New Domains for Applied Quantifier Elimination. CASC 2006, LNCS 4194, pp.295–301, 2006
  2. Thomas Sturm. Redlog Online Resources for Applied Quantifier Elimination. Acta Academiae Aboensis, Ser. B, Mathematica et Physica, 67(2):177–191, 2007
  3. Andreas Dolzmann, Thomas Sturm. Redlog: Computer Algebra Meets Computer Logic. ACM SIGSAM Bulletin 31(2):2–9, 1997