Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis, Logical methods in computer science, vol.8, issue.1, pp.1-32, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00782742
Set coverings and invertibility of functional Galois connections, Idempotent Mathematics and Mathematical Physics Contemporary Mathematics, vol.377, pp.19-51, 2005. ,
DOI : 10.1090/conm/377/06983
URL : https://hal.archives-ouvertes.fr/inria-00000966
The max-plus finite element method for solving deterministic optimal control problems: basic properties and convergence analysis, SIAM J. Control Optim, vol.47, issue.2, pp.817-848, 2008. ,
The Max-Plus Finite Element Method for Solving Deterministic Optimal Control Problems: Basic Properties and Convergence Analysis, SIAM Journal on Control and Optimization, vol.47, issue.2, pp.817-848, 2008. ,
DOI : 10.1137/060655286
URL : https://hal.archives-ouvertes.fr/inria-00071395
Certification of bounds of non-linear functions : the templates method, 2013, To appear in the Proceedings of Conferences on Intelligent Computer Mathematics, CICM 2013 Calculemus ,
Certification of inequalities involving transcendental functions: combining sdp and max-plus approximation, 2013, To appear in the Proceedings of the European Control Conference, p.13 ,
Extending Coq with Imperative Features and Its Application to SAT Verification, Interactive Theorem Proving, pp.83-98, 2010. ,
DOI : 10.1007/978-3-642-14052-5_8
URL : https://hal.archives-ouvertes.fr/inria-00502496
Every planar map is 4-colorable, Illinois Journal of Mathematics, vol.21, pp.429-567, 1977. ,
DOI : 10.1090/s0002-9904-1976-14122-5
URL : http://projecteuclid.org/download/pdf_1/euclid.bams/1183538218
A Numerical Evaluation of Several Stochastic Algorithms on Selected Continuous Global Optimization Test Problems, Journal of Global Optimization, vol.3, issue.3, pp.635-672, 2005. ,
DOI : 10.1007/s10898-004-9972-2
MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions, Journal of Automated Reasoning, vol.7, issue.4, pp.175-205, 2010. ,
DOI : 10.1007/s10817-009-9149-2
Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, 2004. ,
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237
The tracial moment problem and trace-optimization of polynomials, Mathematical Programming, pp.557-578, 2013. ,
DOI : 10.1007/s10107-011-0505-8
URL : https://hal.archives-ouvertes.fr/hal-01119375
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, Proceedings of the 2006 international conference on Types for proofs and programs, TYPES'06, pp.48-62, 2007. ,
DOI : 10.1007/978-3-540-74464-1_4
Chebyshev interpolation polynomial-based tools for rigorous computing, Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, ISSAC '10, pp.147-154, 2010. ,
DOI : 10.1145/1837934.1837966
URL : https://hal.archives-ouvertes.fr/ensl-00472509
Metafunctions: Proving them correct and using them efficiently as new proof procedures, The Correctness Problem in Computer Science, pp.103-84, 1981. ,
Rigorous global search using taylor models, Proceedings of the 2009 conference on Symbolic numeric computation, SNC '09, pp.11-20, 2009. ,
DOI : 10.1145/1577190.1577198
CSDP, A C library for semidefinite programming, Optimization Methods and Software, vol.6, issue.1-4, 1997. ,
DOI : 10.1145/292395.292412
A two-level approach towards lean proof-checking, 1996. ,
DOI : 10.1007/3-540-61780-9_59
Lectures on modern convex optimization: analysis, algorithms, and engineering applications, Society for Industrial and Applied Mathematics, 2001. ,
DOI : 10.1137/1.9780898718829
Handbook of Continued Fractions for Special Functions. SpringerLink: Springer e-Books, 2008. ,
Reduced Vertex Set Result for Interval Semidefinite Optimization Problems, Journal of Optimization Theory and Applications, vol.8, issue.1, pp.17-33, 1007. ,
DOI : 10.1007/s10957-008-9423-1
Designing a Generic Graph Library using ML Functors, The Eighth Symposium on Trends in Functional Programming, pp.1-13, 2007. ,
Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Mathematical Programming, vol.22, issue.3, pp.245-295, 2011. ,
DOI : 10.1007/s10107-009-0286-5
Introduction to Approximation Theory, 1982. ,
Évaluation efficace de fonctions numériques -Outils et exemples. These, 2009. ,
A method for computing lowest eigenvalues of symmetric polynomial differential operators by semidefinite programming. ArXiv e-prints, 2009. ,
Certified and Fast Computation of Supremum Norms of Approximation Errors, 2009 19th IEEE Symposium on Computer Arithmetic, pp.169-176, 2009. ,
DOI : 10.1109/ARITH.2009.18
URL : https://hal.archives-ouvertes.fr/ensl-00334545
Sollya: An Environment for the Development of Numerical Codes, Mathematical Software -ICMS 2010, pp.28-31, 2010. ,
DOI : 10.1007/978-3-642-15582-6_5
URL : https://hal.archives-ouvertes.fr/hal-00761644
Ncsostools: a computer algebra system for symbolic and numerical computation with noncommutative polynomials. Optimization Methods and Software, pp.363-380, 2011. ,
Classification of Injective Factors Cases II 1 , II ??? , III ?? , ?? ??? 1, The Annals of Mathematics, vol.104, issue.1, pp.73-115, 1976. ,
DOI : 10.2307/1971057
Error Bounds for Some Semidefinite Programming Approaches to Polynomial Minimization on the Hypercube, SIAM Journal on Optimization, vol.20, issue.6, pp.3104-3120, 2010. ,
DOI : 10.1137/100790835
A Max-Plus-Based Algorithm for a Hamilton--Jacobi--Bellman Equation of Nonlinear Filtering, SIAM Journal on Control and Optimization, vol.38, issue.3, pp.683-710, 2000. ,
DOI : 10.1137/S0363012998332433
Delta-complete decision procedures for satisfiability over the reals, 1204. ,
Block-diagonal semidefinite programming hierarchies for 0/1 programming, Operations Research Letters, vol.37, issue.1, pp.27-31, 2009. ,
DOI : 10.1016/j.orl.2008.10.003
Proving Equalities in a Commutative Ring Done Right in Coq, Lecture Notes in Computer Science, vol.3603, pp.98-113, 2005. ,
DOI : 10.1007/11541868_7
Curse of dimensionality reduction in max-plus based approximation methods: Theoretical estimates and improved pruning algorithms, IEEE Conference on Decision and Control and European Control Conference, pp.1054-1061, 2011. ,
DOI : 10.1109/CDC.2011.6161386
URL : https://hal.archives-ouvertes.fr/hal-00935266
Computer mathematics. chapter The Four Colour Theorem: Engineering of a Formal Proof, pp.333-333, 2008. ,
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers, Proceedings of IJCAR'06, pp.423-437, 2006. ,
DOI : 10.1007/11814771_36
A Computational Approach to Pocklington Certificates in Type Theory, Functional and Logic Programming, pp.97-113, 2006. ,
DOI : 10.1007/11737414_8
A proof of the kepler conjecture, Math. Intelligencer, vol.16, pp.47-58, 1994. ,
Some algorithms arising in the proof of the kepler conjecture, Discrete and Computational Geometry, pp.489-507, 2003. ,
A proof of the Kepler conjecture, Ann. of Math, vol.162, issue.23, pp.1065-1185, 2005. ,
Introduction to the flyspeck project, Mathematics , Algorithms and Proofs, number 05021 in Dagstuhl Seminar Proceedings Internationales Begegnungs-und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, 2006. ,
The flyspeck project, 2013. ,
Sharpening Interval Computations, Reliable Computing, vol.22, issue.1, pp.21-34, 2006. ,
DOI : 10.1007/s11155-006-2967-6
Verifying Nonlinear Real Formulas Via Sums of Squares, Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, pp.102-118, 2007. ,
DOI : 10.1007/978-3-540-74591-4_9
Major arcs for Goldbach's theorem. ArXiv e-prints, 2013. ,
An interval Newton method, Applied Mathematics and Computation, vol.12, issue.2-3, pp.89-98, 1983. ,
DOI : 10.1016/0096-3003(83)90001-2
POCP: a package for polynomial optimal control problems, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-00325180
Numerical Verification of the Ternary Goldbach Conjecture up to 8.875e30. ArXiv e-prints, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00827998
Generalized Lagrangian Duals and Sums of Squares Relaxations of Sparse Polynomial Optimization Problems, SIAM Journal on Optimization, vol.15, issue.3, 2004. ,
DOI : 10.1137/030601260
Sparsity in sums of squares of polynomials, Mathematical Programming, vol.23, issue.1, 2004. ,
DOI : 10.1007/s10107-004-0554-3
Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients, memory of Wenda Wu, pp.1-15, 1929. ,
DOI : 10.1016/j.jsc.2011.08.002
Multiplication of Multidigit Numbers on Automata, Soviet Physics-Doklady, vol.7, pp.595-596, 1963. ,
Sums of Hermitian Squares and the BMV Conjecture, Journal of Statistical Physics, vol.10, issue.1???4, pp.739-760, 2008. ,
DOI : 10.1007/s10955-008-9632-x
URL : https://hal.archives-ouvertes.fr/hal-00310952
Convergent SDP???Relaxations in Polynomial Optimization with Sparsity, SIAM Journal on Optimization, vol.17, issue.3, pp.822-843 ,
DOI : 10.1137/05064504X
Global Optimization with Polynomials and the Problem of Moments, SIAM Journal on Optimization, vol.11, issue.3, pp.796-817, 2001. ,
DOI : 10.1137/S1052623400366802
Matrix completion problems, Encyclopedia of Optimization, pp.1967-1975, 2009. ,
DOI : 10.1007/0-306-48332-7_271
Differential equations, difference equations and matrix theory, Communications on Pure and Applied Mathematics, vol.7, issue.2, pp.175-194, 1958. ,
DOI : 10.1002/cpa.3160110203
Nonlinear Optimal Control via Occupation Measures and LMI-Relaxations, SIAM Journal on Control and Optimization, vol.47, issue.4, pp.1643-1666, 2008. ,
DOI : 10.1137/070685051
URL : https://hal.archives-ouvertes.fr/hal-00136032
Positivity and optimization for semi-algebraic functions, SIAM Journal on Optimization, vol.20, issue.6, pp.3364-3383, 2010. ,
Equivalent Forms of the Bessis???Moussa???Villani Conjecture, Journal of Statistical Physics, vol.115, issue.1/2, pp.185-190, 2004. ,
DOI : 10.1023/B:JOSS.0000019811.15510.27
Convex underestimators of polynomials, Journal of Global Optimization, vol.56, issue.1, pp.1-25, 2013. ,
An Introduction to Gamma-Convergence, 1993. ,
On the Generation of Positivstellensatz Witnesses in Degenerate Cases, Interactive Theorem Proving (ITP), pp.249-264, 2011. ,
DOI : 10.1137/1038003
URL : https://hal.archives-ouvertes.fr/hal-00594761
Max-plus methods for nonlinear control and estimation. Systems & Control: Foundations & Applications, Birkhäuser Boston Inc, 2006. ,
A Curse-of-Dimensionality-Free Numerical Method for Solution of Certain HJB PDEs, SIAM Journal on Control and Optimization, vol.46, issue.4, pp.1239-1276, 2007. ,
DOI : 10.1137/040610830
Curse-of-complexity attenuation in the curse-of-dimensionality-free method for HJB PDEs, 2008 American Control Conference ,
DOI : 10.1109/ACC.2008.4587234
Floating-point arithmetic in the coq system Information and Computation, <ce:title>Special Issue: 8th Conference on Real Numbers and Computers<, pp.14-23, 2012. ,
Extensions of affine arithmetic: Application to unconstrained global optimization, 1999. ,
The Chebyshev Polynomials, 2003. ,
DOI : 10.1201/9781420036114
Intsolver: An interval based toolbox for global optimization, 2009. ,
Modern general topology. Bibliotheca mathematica, 1974. ,
Interior Point Polynomial Methods in Convex Programming: Theory and Applications, Society for Industrial and Applied Mathematics, 1994. ,
On the complexity of Putinar's Positivstellensatz, Journal of Complexity, vol.23, issue.1, pp.135-150, 2007. ,
DOI : 10.1016/j.jco.2006.07.002
Hyperbolic Polynomials and Generalized Clifford Algebras. ArXiv e-prints, 2012. ,
DOI : 10.1007/s00454-014-9598-1
URL : http://arxiv.org/abs/1207.3159
Computing sum of squares decompositions with rational coefficients, Theoretical Computer Science, vol.409, issue.2, pp.269-281, 2008. ,
DOI : 10.1016/j.tcs.2008.09.025
Minimizing polynomial functions, DIMACS Ser. Discrete Math. Theoret. Comput. Sci. Amer. Math. Soc, vol.60, pp.83-99, 2003. ,
Convex Analysis. Princeton mathematical series, 1970. ,
Exploiting Symmetries in SDP-Relaxations for Polynomial Optimization, Mathematics of Operations Research, vol.38, issue.1, 2011. ,
DOI : 10.1287/moor.1120.0558
On the complexity of Schm??dgen's Positivstellensatz, Journal of Complexity, vol.20, issue.4, pp.529-543, 2004. ,
DOI : 10.1016/j.jco.2004.01.005
Optimization of Polynomials on Compact Semialgebraic Sets, SIAM Journal on Optimization, vol.15, issue.3, pp.805-825, 2005. ,
DOI : 10.1137/S1052623403431779
Reduced-complexity numerical method for optimal gate synthesis, Physical Review A, vol.82, issue.4, p.42319, 2010. ,
DOI : 10.1103/PhysRevA.82.042319
Formal verification of nonlinear inequalities with taylor interval approximations. CoRR, abs, 1301. ,
Ajouter des entiers machine à coq, 2006. ,
Scalable Analysis of Linear Systems Using Mathematical Programming, Proc. of Verification, Model Checking and Abstract Interpretation (VMCAI), pp.21-47, 2005. ,
DOI : 10.1007/978-3-540-30579-8_2
Proof of the BMV Conjecture. ArXiv e-prints, 2011. ,
Using sedumi 1.02, a matlab toolbox for optimization over symmetric cones, 1998. ,
Semidefinite Programming, SIAM Review, vol.38, issue.1, pp.49-95, 1994. ,
DOI : 10.1137/1038003
Algorithm 883, ACM Transactions on Mathematical Software, vol.35, issue.2, 2008. ,
DOI : 10.1145/1377612.1377619
Sums of Squares and Semidefinite Program Relaxations for Polynomial Optimization Problems with Structured Sparsity, SIAM Journal on Optimization, vol.17, issue.1, pp.218-242, 2006. ,
DOI : 10.1137/050623802
A highperformance software package for semidefinite programs : Sdpa7, Dept. of Information Sciences, 2010. ,
Rigorous Global Optimization, 2008. ,