{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:55:39Z","timestamp":1763459739797,"version":"3.45.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,18]],"date-time":"2017-01-18T00:00:00Z","timestamp":1484697600000},"content-version":"vor","delay-in-days":366,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR0011-12-C-0123"],"award-info":[{"award-number":["HR0011-12-C-0123"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,18]]},"DOI":"10.1145\/2854065.2854066","type":"proceedings-article","created":{"date-parts":[[2016,1,12]],"date-time":"2016-01-12T08:18:57Z","timestamp":1452586737000},"page":"15-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["A unified Coq framework for verifying C programs with floating-point computations"],"prefix":"10.1145","author":[{"given":"Tahina","family":"Ramananandro","sequence":"first","affiliation":[{"name":"Reservoir Labs, USA"}]},{"given":"Paul","family":"Mountcastle","sequence":"additional","affiliation":[{"name":"Reservoir Labs, USA"}]},{"given":"Beno\u00eet","family":"Meister","sequence":"additional","affiliation":[{"name":"Reservoir Labs, USA"}]},{"given":"Richard","family":"Lethin","sequence":"additional","affiliation":[{"name":"Reservoir Labs, USA"}]}],"member":"320","published-online":{"date-parts":[[2016,1,18]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"1","volume":"754","author":"Floating-Point Arithmetic IEEE","year":"2008","unstructured":"IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2008, pages 1\u201370, Aug 2008..","journal-title":"IEEE Std"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/2670099"},{"key":"e_1_3_2_1_4_1","unstructured":"ISBN 110704801X 9781107048010."},{"key":"e_1_3_2_1_5_1","volume-title":"PERFECT (Power Efficiency Revolution For Embedded Computing Technologies) Benchmark Suite Manual","author":"Barker K.","year":"2013","unstructured":"K. Barker, T. Benson, D. Campbell, D. Ediger, R. Gioiosa, A. Hoisie, D. Kerbyson, J. Manzano, A. Marquez, L. Song, N. Tallent, and A. Tumeo. PERFECT (Power Efficiency Revolution For Embedded Computing Technologies) Benchmark Suite Manual. Pacific Northwest National Laboratory and Georgia Tech Research Institute, December 2013. http:\/\/hpc.pnnl.gov\/projects\/PERFECT\/."},{"key":"e_1_3_2_1_6_1","unstructured":"P. Baudin F. Bobot R. Bonichon L. Correnson P. Cuoq Z. Dargaye J.-C. Filli\u02c6atre P. Hermann F. Kirchner M. Lemerre. C. March\u00e9 B. Monate Y. Moy A. Pacalet V. Prevosto J. Signoles and B. Yakobowski. Frama-C. http:\/\/frama-c.com 2007\u20132015."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/2831143.2831157"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_3_2_1_9_1","unstructured":"Donn\u00e9es compl\u00e9mentaires http:\/\/coq.inria.fr."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2011.40"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02614-0_10"},{"key":"e_1_3_2_1_13_1","unstructured":"ISBN 978-3-642-02613-3.. URL http:\/\/dx.doi.org\/10.1007\/ 978-3-642-02614-0_10."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9255-4"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-014-9317-x"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/993483"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","unstructured":"N. Brisebarre M. Jolde E. Martin-Dorel M. Mayero J.-M. Muller I. Paca L. Rideau and L. Th\u00e9ry. Rigorous polynomial approximation using Taylor models in Coq. In A. Goodloe and S. Person editors NASA Formal Methods volume 7226 of Lecture Notes in Computer Science pages 85\u201399. Springer Berlin Heidelberg 2012. ISBN 978- 3-642-28890-6. 10.1007\/978-3-642-28891-3_9","DOI":"10.1007\/978-3-642-28891-3_9"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1888390.1888397"},{"key":"e_1_3_2_1_19_1","unstructured":"T. Coq development team. The Coq proof assistant. http:\/\/coq. inria.fr 1984\u20132015."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04570-7_6"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/83.199920"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_3_2_1_24_1","unstructured":"2103719."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_3"},{"key":"e_1_3_2_1_26_1","unstructured":"M. Grant and S. Boyd. CVX: Matlab software for disciplined convex programming version 2.0 beta. http:\/\/cvxr.com\/cvx Sept. 2013."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1137\/0914050"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/363707.363723"},{"key":"e_1_3_2_1_30_1","unstructured":". URL http:\/\/doi.acm.org\/10.1145\/363707.363723."},{"key":"e_1_3_2_1_31_1","unstructured":"O. Kupriianova and C. Lauter. Metalibm. http:\/\/lipforge. ens-lyon.fr\/www\/metalibm\/ 2013."},{"key":"e_1_3_2_1_32_1","volume-title":"http:\/\/compcert.inria.fr","author":"Leroy X.","year":"2005","unstructured":"X. Leroy. Compcert. http:\/\/compcert.inria.fr, 2005\u20132015."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_34_1","unstructured":"G. Melquiond. De l\u2019arithm\u00e9tique d\u2019intervalles \u00e0 la certification de programmes. PhD thesis \u00c9cole Normale Sup\u00e9rieure de Lyon Lyon France 2006. URL http:\/\/www.lri.fr\/~melquion\/doc\/ 06-these.pdf."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_2"},{"key":"e_1_3_2_1_36_1","volume-title":"http:\/\/coq-interval.gforge. inria.fr\/","author":"Melquiond G.","year":"2008","unstructured":"G. Melquiond. Coq-interval. http:\/\/coq-interval.gforge. inria.fr\/, 2008\u20132015."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/261217"},{"key":"e_1_3_2_1_38_1","unstructured":"J. M. Muller F. D. Dinechin et al. CRlibm: Correctly Rounded mathematical library. http:\/\/lipforge.ens-lyon.fr\/www\/crlibm\/ 2005\u20132010."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/2388996.2389034"},{"key":"e_1_3_2_1_40_1","volume-title":"Synthetic aperture radar signal processing","author":"Soumekh M.","year":"1999","unstructured":"M. Soumekh. Synthetic aperture radar signal processing. New York: Wiley, 1999."},{"key":"e_1_3_2_1_41_1","volume-title":"Prentice-Hall","author":"Sterbenz P. H.","year":"1973","unstructured":"P. H. Sterbenz. Floating-point computation. Englewood Cliffs ; London : Prentice-Hall, 1973. ISBN 0133224953."},{"key":"e_1_3_2_1_42_1","volume-title":"a MATLAB toolbox for optimization over symmetric cones. Optimization Methods and Software, 11\u2013 12:625\u2013653","author":"Sturm J. F.","year":"1999","unstructured":"J. F. Sturm. Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optimization Methods and Software, 11\u2013 12:625\u2013653, 1999. Version 1.3 available from http:\/\/coral.ie. lehigh.edu\/~newsedumi\/?page_id=20."},{"volume-title":"FLUCTUAT","author":"Vedrine F.","key":"e_1_3_2_1_43_1","unstructured":"F. Vedrine, E. Goubault, and S. Putot. FLUCTUAT. http:\/\/www. lix.polytechnique.fr\/Labo\/Sylvie.Putot\/fluctuat.html, 2001\u20132015."}],"event":{"name":"CPP 2016: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"St. Petersburg FL USA","acronym":"CPP 2016"},"container-title":["Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854066","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2854065.2854066","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2854065.2854066","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:52:08Z","timestamp":1763459528000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854066"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,18]]},"references-count":43,"alternative-id":["10.1145\/2854065.2854066","10.1145\/2854065"],"URL":"https:\/\/doi.org\/10.1145\/2854065.2854066","relation":{},"subject":[],"published":{"date-parts":[[2016,1,18]]},"assertion":[{"value":"2016-01-18","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}