{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T16:49:59Z","timestamp":1791218999849,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":54,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,1,8]],"date-time":"2014-01-08T00:00:00Z","timestamp":1389139200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,1,8]]},"DOI":"10.1145\/2535838.2535874","type":"proceedings-article","created":{"date-parts":[[2014,1,14]],"date-time":"2014-01-14T08:40:06Z","timestamp":1389688806000},"page":"235-248","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":111,"title":["Sound compilation of reals"],"prefix":"10.1145","author":[{"given":"Eva","family":"Darulova","sequence":"first","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,1,8]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"Caliper open source framework. http:\/\/code.google.com\/p\/caliper\/.  Caliper open source framework. http:\/\/code.google.com\/p\/caliper\/."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2010.2042980"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1879021.1879024"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_11"},{"key":"e_1_3_2_2_5_1","unstructured":"D. H. Bailey Y. Hida X. S. Li and B. Thompson. C++\/Fortran-90 double-double and quad-double package. http:\/\/crdlegacy.lbl.gov\/?dhbailey\/mpdist\/ 2013.  D. H. Bailey Y. Hida X. S. Li and B. Thompson. C++\/Fortran-90 double-double and quad-double package. http:\/\/crdlegacy.lbl.gov\/?dhbailey\/mpdist\/ 2013."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254118"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2489837.2489838"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2012.91"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9196-8"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706308"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025131"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_21"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048094"},{"key":"e_1_3_2_2_16_1","volume-title":"RV","author":"Darulova E.","year":"2012","unstructured":"E. Darulova and V. Kuncak . Certifying Solutions for Numerical Constraints . In RV , 2012 . E. Darulova and V. Kuncak. Certifying Solutions for Numerical Constraints. In RV, 2012."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/2555754.2555776"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2010.128"},{"key":"e_1_3_2_2_19_1","volume-title":"IMPA\/CNPq","author":"de Figueiredo L. H.","year":"1997","unstructured":"L. H. de Figueiredo and J. Stolfi . Self-Validated Numerical Methods and Applications . IMPA\/CNPq , Brazil , 1997 . L. H. de Figueiredo and J. Stolfi. Self-Validated Numerical Methods and Applications. IMPA\/CNPq, Brazil, 1997."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04570-7_6"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_5"},{"key":"e_1_3_2_2_23_1","volume-title":"CFV\/IJCAR","author":"Duracz J. A.","year":"2008","unstructured":"J. A. Duracz and M. Konecny . Polynomial function enclosures and floating point software verification . In CFV\/IJCAR , 2008 . J. A. Duracz and M. Konecny. Polynomial function enclosures and floating point software verification. In CFV\/IJCAR, 2008."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_4"},{"key":"e_1_3_2_2_25_1","volume-title":"FMCAD","author":"Gao S.","year":"2010","unstructured":"S. Gao , M. Ganai , F. Ivancic , A. Gupta , S. Sankaranarayanan , and E. Clarke . Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems . In FMCAD , 2010 . S. Gao, M. Ganai, F. Ivancic, A. Gupta, S. Sankaranarayanan, and E. Clarke. Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. In FMCAD, 2010."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_22"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/103162.103163"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_5"},{"key":"e_1_3_2_2_29_1","volume-title":"FMCAD","author":"Haller L.","year":"2012","unstructured":"L. Haller , A. Griggio , M. Brain , and D. Kroening . Deciding floatingpoint logic with systematic abstraction . In FMCAD , 2012 . L. Haller, A. Griggio, M. Brain, and D. Kroening. Deciding floatingpoint logic with systematic abstraction. In FMCAD, 2012."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/11757283_8"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2010.5558622"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45234-8_119"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_27"},{"key":"e_1_3_2_2_35_1","volume-title":"Technical report","author":"Kahan W.","year":"2000","unstructured":"W. Kahan . Miscalculating Area and Angles of a Needle-like Triangle . Technical report , University of California Berkeley , 2000 . W. Kahan. Miscalculating Area and Angles of a Needle-like Triangle. Technical report, University of California Berkeley, 2000."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/1928028.1928039"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926387"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1772954.1772987"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2010.5558629"},{"key":"e_1_3_2_2_41_1","volume-title":"International Journal of Pure and Applied Mathematics, 4","author":"Makino K.","year":"2003","unstructured":"K. Makino and M. Berz . Taylor Models and Other Validated Functional Inclusion Methods . International Journal of Pure and Applied Mathematics, 4 , 2003 . K. Makino and M. Berz. Taylor Models and Other Validated Functional Inclusion Methods. International Journal of Pure and Applied Mathematics, 4, 2003."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_2"},{"key":"e_1_3_2_2_43_1","unstructured":"R. Moore. Interval Analysis. Prentice-Hall 1966.  R. Moore. Interval Analysis. Prentice-Hall 1966."},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"crossref","DOI":"10.1007\/b98868","volume-title":"Mathematical Biology","author":"Murray J. D.","year":"2002","unstructured":"J. D. Murray . Mathematical Biology . Springer , 2002 . J. D. Murray. Mathematical Biology. Springer, 2002."},{"key":"e_1_3_2_2_45_1","volume-title":"Artima Incorporation","author":"Odersky M.","year":"2008","unstructured":"M. Odersky , L. Spoon , and B. Venners . Programming in Scala: A Comprehensive Step-by-step Guide . Artima Incorporation , 2008 . M. Odersky, L. Spoon, and B. Venners. Programming in Scala: A Comprehensive Step-by-step Guide. Artima Incorporation, 2008."},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2013.35"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33558-7_43"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-12430-3","volume-title":"Scientific Computing with MATLAB and Octave","author":"Quarteroni A.","year":"2010","unstructured":"A. Quarteroni , F. Saleri , and P. Gervasio . Scientific Computing with MATLAB and Octave . Springer , 3 rd edition, 2010 . A. Quarteroni, F. Saleri, and P. Gervasio. Scientific Computing with MATLAB and Octave. Springer, 3rd edition, 2010.","edition":"3"},{"key":"e_1_3_2_2_49_1","volume-title":"An SMT-LIB Theory of Binary Floating-Point Arithmetic. In Informal proceedings of SMT at FLoC","author":"R\u00fcmmer P.","year":"2010","unstructured":"P. R\u00fcmmer and T. Wahl . An SMT-LIB Theory of Binary Floating-Point Arithmetic. In Informal proceedings of SMT at FLoC , 2010 . P. R\u00fcmmer and T. Wahl. An SMT-LIB Theory of Binary Floating-Point Arithmetic. In Informal proceedings of SMT at FLoC, 2010."},{"key":"e_1_3_2_2_50_1","volume-title":"Computer Physics Communications","author":"Scott N.","year":"2007","unstructured":"N. Scott , F. J\u00e9z\u00e9quel , C. Denis , and J.-M. Chesneaux . Numerical 'health check' for scientific codes: the CADNA approach . Computer Physics Communications , 2007 . N. Scott, F. J\u00e9z\u00e9quel, C. Denis, and J.-M. Chesneaux. Numerical 'health check' for scientific codes: the CADNA approach. Computer Physics Communications, 2007."},{"key":"e_1_3_2_2_51_1","first-page":"754","year":"2008","unstructured":"I. C. Society. IEEE Standard for Floating-Point Arithmetic. IEEE Std 754 - 2008 , 2008 . I. C. Society. IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2008, 2008.","journal-title":"I. C. Society. IEEE Standard for Floating-Point Arithmetic. IEEE Std"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831724"},{"key":"e_1_3_2_2_53_1","volume-title":"CoRR","author":"Westbrook E. M.","year":"2013","unstructured":"E. M. Westbrook and S. Chaudhuri . A Semantics for Approximate Program Transformations . CoRR , 2013 . E. M. Westbrook and S. Chaudhuri. A Semantics for Approximate Program Transformations. CoRR, 2013."},{"key":"e_1_3_2_2_54_1","volume-title":"Springer","author":"Woodford C.","year":"2012","unstructured":"C. Woodford and C. Phillips . Numerical Methods with Worked Examples, volume 2nd . Springer , 2012 . C. Woodford and C. Phillips. Numerical Methods with Worked Examples, volume 2nd. Springer, 2012."}],"event":{"name":"POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"San Diego California USA","acronym":"POPL '14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535874","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2535838.2535874","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:06Z","timestamp":1750219806000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535874"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1,8]]},"references-count":54,"alternative-id":["10.1145\/2535838.2535874","10.1145\/2535838"],"URL":"https:\/\/doi.org\/10.1145\/2535838.2535874","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2578855.2535874","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,1,8]]},"assertion":[{"value":"2014-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}