{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,2]],"date-time":"2025-12-02T03:15:27Z","timestamp":1764645327080,"version":"3.41.0"},"publisher-location":"New York, New York, USA","reference-count":13,"publisher":"ACM Press","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-12-INSE-0007"],"award-info":[{"award-number":["ANR-12-INSE-0007"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100007267","name":"Centre International de Mathematiques et Informatique de Toulouse","doi-asserted-by":"publisher","award":["ANR-11-LABX-0040-CIMI"],"award-info":[{"award-number":["ANR-11-LABX-0040-CIMI"]}],"id":[{"id":"10.13039\/501100007267","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1145\/3018610.3018622","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T21:20:29Z","timestamp":1482441629000},"page":"90-99","source":"Crossref","is-referenced-by-count":9,"title":["A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations"],"prefix":"10.1145","author":[{"given":"\u00c9rik","family":"Martin-Dorel","sequence":"first","affiliation":[{"name":"IRIT, France \/ Paul Sabatier University, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Roux","sequence":"additional","affiliation":[{"name":"ONERA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"key-10.1145\/3018610.3018622-1","doi-asserted-by":"crossref","unstructured":"A. Adjé, P. Garoche, and V. Magron. Property-based polynomial invariant generation using sums-of-squares optimization. In S. Blazy and T. Jensen, editors, Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings, volume 9291 of LNCS, pages 235– 251. Springer, 2015. ISBN 978-3-662-48287-2. doi: 10.1007\/ 978-3-662-48288-9_14.","DOI":"10.1007\/978-3-662-48288-9_14"},{"key":"key-10.1145\/3018610.3018622-2","doi-asserted-by":"crossref","unstructured":"1356057. S. Bernard, Y. Bertot, L. Rideau, and P. Strub. Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. In J. Avigad and A. Chlipala, editors, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016, pages 76–87. ACM, 2016. ISBN 978- 1-4503-4127-1. doi: 10.1145\/2854065.2854072.","DOI":"10.1145\/2854065.2854072"},{"key":"key-10.1145\/3018610.3018622-3","doi-asserted-by":"crossref","unstructured":"B. Borchers. CSDP, a C library for semidefinite programming. Optimization Methods and Software, 11(1-4), 1999.","DOI":"10.1080\/10556789908805765"},{"key":"key-10.1145\/3018610.3018622-4","doi-asserted-by":"crossref","unstructured":"C. Cohen, M. Dénès, and A. Mörtberg. Refinements for free! In G. Gonthier and M. Norrish, editors, Certified Programs and Proofs, volume 8307 of LNCS, pages 147–162. Springer, 2013. ISBN 978-3-319-03544-4.","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"key-10.1145\/3018610.3018622-5","unstructured":"The Coq proof assistant reference manual. The Coq development team, 2016."},{"key":"key-10.1145\/3018610.3018622-6","doi-asserted-by":"crossref","unstructured":"J. Harrison. Verifying nonlinear real formulas via sums of squares. In TPHOLs 2007, volume 4732 of LNCS, pages 102–118. Springer, 2007.","DOI":"10.1007\/978-3-540-74591-4_9"},{"key":"key-10.1145\/3018610.3018622-7","unstructured":"IEEE Computer Society. IEEE Standard for Floating-Point Arithmetic. IEEE Standard 754-2008, 2008."},{"key":"key-10.1145\/3018610.3018622-8","doi-asserted-by":"crossref","unstructured":"J. B. Lasserre. Global optimization with polynomials and the problem of moments. SIAM Journal on Optimization, 11(3): 796–817, 2001. doi: 10.1137\/S1052623400366802.","DOI":"10.1137\/S1052623400366802"},{"key":"key-10.1145\/3018610.3018622-9","unstructured":"doi: 10.1007\/ s10817-015-9339-z."},{"key":"key-10.1145\/3018610.3018622-10","doi-asserted-by":"crossref","unstructured":"S. M. Rump. Verification methods: Rigorous results using floatingpoint arithmetic. Acta Numerica, 19, 2010.","DOI":"10.1145\/1837934.1837937"},{"key":"key-10.1145\/3018610.3018622-11","doi-asserted-by":"crossref","unstructured":"A. Solovyev and T. C. Hales. Formal verification of nonlinear inequalities with Taylor interval approximations. In NASA Formal Methods, volume 7871 of LNCS, pages 383–397, 2013.","DOI":"10.1007\/978-3-642-38088-4_26"},{"key":"key-10.1145\/3018610.3018622-12","doi-asserted-by":"crossref","unstructured":"L. Vandenberghe and S. P. Boyd. Semidefinite programming. SIAM Review, 38(1):49–95, 1996.","DOI":"10.1137\/1038003"},{"key":"key-10.1145\/3018610.3018622-13","unstructured":"doi: 10.1137\/ 1038003."}],"event":{"number":"2017","sponsor":["SIGLOG, ACM Special Interest Group on Logic and Computation","SIGPLAN, ACM Special Interest Group on Programming Languages"],"acronym":"CPP 2017","name":"the 6th ACM SIGPLAN Conference","start":{"date-parts":[[2017,1,16]]},"location":"Paris, France","end":{"date-parts":[[2017,1,17]]}},"container-title":["Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2017"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018622","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/dl.acm.org\/ft_gateway.cfm?id=3018622&ftid=1823008&dwn=1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:59Z","timestamp":1750220639000},"score":1,"resource":{"primary":{"URL":"http:\/\/dl.acm.org\/citation.cfm?doid=3018610.3018622"}},"subtitle":[],"proceedings-subject":"Certified Programs and Proofs","short-title":[],"issued":{"date-parts":[[2017]]},"references-count":13,"URL":"https:\/\/doi.org\/10.1145\/3018610.3018622","relation":{},"subject":[],"published":{"date-parts":[[2017]]}}}