Selected Redlog References

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