An alternative method for linear programming, Mathematical Proceedings of the Cambridge Philosophical Society, vol.50, issue.04, pp.513-523, 1954. ,
DOI : 10.1017/S0305004100029650
Integrating decision procedures for temporal verification, 1999. ,
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic, IJCAR 2012, pp.67-81, 2012. ,
DOI : 10.1007/978-3-642-31365-3_8
URL : https://hal.archives-ouvertes.fr/hal-00687640
Convex Optimization, 2004. ,
Linear Integer Arithmetic Revisited, LNCS, vol.9195, pp.25-623, 2015. ,
DOI : 10.1007/978-3-319-21401-6_42
URL : https://hal.archives-ouvertes.fr/hal-01239394
Computing a complete basis for equalities implied by a system of LRA constraints, SMT 2016, pp.15-30, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01403214
Fast Cube Tests for LIA Constraint Solving, IJCAR 2016, 2016. ,
DOI : 10.1145/322276.322287
URL : https://hal.archives-ouvertes.fr/hal-01403200
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis, AMAI, vol.55, issue.1, pp.63-99, 2009. ,
Cuts from proofs: A complete and practical technique for solving linear inequalities over integers, CAV, LNCS, pp.233-247, 2009. ,
Real Quantifier Elimination in Practice, Algorithmic Algebra and Number Theory, pp.221-247, 1999. ,
DOI : 10.1007/978-3-642-59932-3_11
Yices??2.2, CAV 2014, 2014. ,
DOI : 10.1007/978-3-319-08867-9_49
A fast linear-arithmetic solver for DPLL(T) Extended version: Integrating simplex with DPLL(T), CAV, pp.81-94, 2006. ,
SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers, SAT 2008, pp.77-90, 2008. ,
DOI : 10.1007/978-3-540-79719-7_8
URL : https://hal.archives-ouvertes.fr/inria-00358813
A practical approach to satisfiability modulo linear integer arithmetic, JSAT, vol.8, issue.12, pp.1-27, 2012. ,
Efficient Heuristic Procedures for Integer Linear Programming with an Interior, Operations Research, vol.17, issue.4, pp.600-637, 1969. ,
DOI : 10.1287/opre.17.4.600
Cutting to the Chase, Journal of Automated Reasoning, vol.28, issue.4, pp.79-108, 2013. ,
DOI : 10.1145/125826.125848
Covering minima and lattice point free convex bodies, FSTTCS, pp.193-213, 1986. ,
A new polynomial-time algorithm for linear programming, Combinatorica, vol.244, issue.S, pp.373-396, 1984. ,
DOI : 10.1007/BF02579150
The dual method of solving the linear programming problem, Naval Research Logistics Quarterly, vol.1, issue.1, pp.36-47, 1954. ,
DOI : 10.1002/nav.3800010107
Applying Linear Quantifier Elimination, The Computer Journal, vol.36, issue.5, pp.450-462, 1993. ,
DOI : 10.1093/comjnl/36.5.450
Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol.4963, pp.337-340, 2008. ,
On the complexity of integer programming, Journal of the ACM, vol.28, issue.4, pp.765-768, 1981. ,
DOI : 10.1145/322276.322287
The Omega test: a fast and practical integer programming algorithm for dependence analysis, Proceedings of the 1991 ACM/IEEE conference on Supercomputing , Supercomputing '91, pp.4-13, 1991. ,
DOI : 10.1145/125826.125848
Approaches to the incremental detection of implicit equalities with the revised simplex method, PLILP 1998, pp.481-496, 1998. ,
DOI : 10.1007/BFb0056634
Solving linear arithmetic constraints, Tech. rep., SRI International, 2004. ,
Theory of Linear and Integer Programming, 1986. ,
Real quadratic quantifier elimination in risa/asir, 1996. ,
Identifying Redundant Constraints and Implicit Equalities in Systems of Linear Constraints, Management Science, vol.29, issue.10, pp.1209-1222, 1983. ,
DOI : 10.1287/mnsc.29.10.1209
Standard forms for rational linear arithmetic in constraint logic programming, Annals of Mathematics and Artificial Intelligence, vol.5, issue.2-4, pp.303-319, 1992. ,
DOI : 10.2140/pjm.1955.5.183