B. Akbarpour and L. C. Paulson, MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions, Journal of Automated Reasoning, vol.7, issue.4, pp.175-205, 2010.
DOI : 10.1145/1183278.1183282
URL : http://www.cl.cam.ac.uk/~lp15/papers/Arith/MetiTarski-jar.pdf

C. Barrett, D. Kroening, and T. Melham, Problem solving for the 21st century: efficient solvers for satisfiability modulo theories, and Smith Institute for Industrial Mathematics and System Engineering Knowledge Transfer Report, 2014.

C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli, Satisfiability modulo theories Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.185, pp.825-885, 2009.

F. Benhamou and L. Granvilliers, Continuous and Interval Constraints, Handbook of Constraint Programming, pp.571-604, 2006.
DOI : 10.1016/S1574-6526(06)80020-9
URL : https://hal.archives-ouvertes.fr/hal-00480814

M. Bofill, R. Nieuwenhuis, A. Oliveras, E. Rodríguez-carbonell, and A. Rubio, The Barcelogic SMT Solver, CAV 2008, pp.294-298, 2008.
DOI : 10.1007/978-3-540-70545-1_27

T. Bouton, B. Caminha, D. De-oliveira, D. Déharbe, and P. Fontaine, veriT: An Open, Trustable and Efficient SMT-Solver, CADE 2009, pp.151-156, 2009.
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634

B. Buchberger, Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. Doctoral dissertation, Austria, 1965.

A. Cimatti, A. Griggio, A. Irfan, M. Roveri, and R. Sebastiani, Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF, TACAS 2017, pp.58-75, 2017.
DOI : 10.1007/978-3-319-21690-4_34

F. Corzilius, U. Loup, S. Junges, and E. Abrahám, SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox
DOI : 10.1007/978-3-642-31612-8_35

G. B. Dantzig, Linear Programming and Extensions, 1963.
DOI : 10.1515/9781400884179

B. Dutertre and L. De-moura, A Fast Linear-Arithmetic Solver for DPLL(T), CAV 2006, pp.81-9410, 2006.
DOI : 10.1007/11817963_11

H. Errami, M. Eiswirth, D. Grigoriev, W. M. Seiler, T. Sturm et al., Detection of Hopf bifurcations in chemical reaction networks using convex coordinates, Journal of Computational Physics, vol.291, pp.279-302, 2015.
DOI : 10.1016/j.jcp.2015.02.050
URL : https://hal.archives-ouvertes.fr/hal-01239486

M. Fränzle, C. Herde, T. Teige, S. Ratschan, and T. Schubert, Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure, J. Satisf. Boolean Model. Comput, vol.1, pp.209-236, 2007.

C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-kamp, R. Thiemann et al., SAT Solving for Termination Analysis with Polynomial Interpretations, SAT 2007, pp.340-354
DOI : 10.1007/978-3-540-72788-0_33

M. Ganai and F. Ivancic, Efficient decision procedure for non-linear arithmetic constraints using CORDIC, 2009 Formal Methods in Computer-Aided Design, pp.61-68, 2009.
DOI : 10.1109/FMCAD.2009.5351140

H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, DPLL(T): Fast Decision Procedures, CAV 2004, pp.175-188, 2004.
DOI : 10.1007/978-3-540-27813-9_14
URL : ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/GanHNOT-CAV-04.pdf

S. Gao, S. Kong, and E. M. Clarke, Satisfiability modulo ODEs, Formal Methods in Computer-Aided Design (FMCAD) 2013, pp.105-112, 2013.

S. Gao, S. Kong, and E. M. Clarke, dReal: An SMT Solver for Nonlinear Theories over the Reals, CADE 2013, pp.208-21410, 2013.
DOI : 10.1007/978-3-642-38574-2_14

L. Granvilliers and F. Benhamou, Algorithm 852, ACM Transactions on Mathematical Software, vol.32, issue.1, pp.138-156, 2006.
DOI : 10.1145/1132973.1132980
URL : https://hal.archives-ouvertes.fr/hal-00480813

D. Jovanovi´cjovanovi´c and L. De-moura, Solving non-linear arithmetic, IJCAR 2012, pp.339-354, 2012.

N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica, vol.244, issue.S, pp.373-395, 1984.
DOI : 10.1007/BF02579150
URL : http://www.eecs.berkeley.edu/~orecchia/working/karmakar full.pdf

L. Khachiyan, Polynomial algorithms in linear programming, USSR Computational Mathematics and Mathematical Physics, vol.20, issue.1, pp.53-72, 1980.
DOI : 10.1016/0041-5553(80)90061-0

G. O. Passmore, Combined decision procedures for nonlinear arithmetics, real and complex. Dissertation, 2011.

G. O. Passmore and P. B. Jackson, Combined Decision Techniques for the Existential Theory of the Reals, CICM 2009, pp.122-137, 2009.
DOI : 10.1007/s002000050055

S. Ratschan, Efficient solving of quantified inequality constraints over the real numbers, ACM Transactions on Computational Logic, vol.7, issue.4, pp.723-748, 2006.
DOI : 10.1145/1183278.1183282

A. Schrijver, Theory of Linear and Integer Programming, 1986.

T. Sturm, Subtropical Real Root Finding, Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation, ISSAC '15, pp.347-354, 2015.
DOI : 10.1007/s11538-010-9618-0
URL : https://hal.archives-ouvertes.fr/hal-01239489

V. X. Tung, T. Van-khanh, and M. Ogawa, raSAT: an SMT solver for polynomial constraints, IJCAR 2016, pp.228-23710, 2016.
DOI : 10.1007/978-3-319-40229-1_16

H. Zankl and A. Middeldorp, Satisfiability of Non-linear (Ir)rational??Arithmetic, LPAR 2010, pp.481-500
DOI : 10.1007/s10817-009-9131-z
URL : http://cl-informatik.uibk.ac.at/users/hzankl/new/publications/ZA10_02.pdf