{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T02:13:28Z","timestamp":1743041608505,"version":"3.40.3"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319633893"},{"type":"electronic","value":"9783319633909"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"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.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_22","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"419-435","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT"],"prefix":"10.1007","author":[{"given":"Sylvain","family":"Conchon","sequence":"first","affiliation":[]},{"given":"Mohamed","family":"Iguernlala","sequence":"additional","affiliation":[]},{"given":"Kailiang","family":"Ji","sequence":"additional","affiliation":[]},{"given":"Guillaume","family":"Melquiond","sequence":"additional","affiliation":[]},{"given":"Cl\u00e9ment","family":"Fumex","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"22_CR1","unstructured":"IEEE Standard for Floating-Point Arithmetic. Technical report. IEEE, August 2008"},{"key":"22_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015)"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: Antelo, E., Hough, D., Ienne, P. (eds.) Proceedings of the 20th IEEE Symposium on Computer Arithmetic, T\u00fcbingen, Germany, pp. 243\u2013252 (2011)","DOI":"10.1109\/ARITH.2011.40"},{"issue":"2","key":"22_CR4","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10703-013-0203-7","volume":"45","author":"M Brain","year":"2014","unstructured":"Brain, M., D\u2019Silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. Form. Methods Syst. Des. 45(2), 213\u2013245 (2014). doi:10.1007\/s10703-013-0203-7","journal-title":"Form. Methods Syst. Des."},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Brain, M., Tinelli, C., R\u00fcmmer, P., Wahl, T.: An automatable formal semantics for IEEE-754 floating-point arithmetic. In: Muller, J.-M., Tisserand, A., Villalba, J. (eds.) Proceedings of the 22nd IEEE Symposium on Computer Arithmetic, pp. 160\u2013167. IEEE, Washington, D.C. (2015)","DOI":"10.1109\/ARITH.2015.26"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-44755-5_13","volume-title":"Theorem Proving in Higher Order Logics","author":"M Daumas","year":"2001","unstructured":"Daumas, M., Rideau, L., Th\u00e9ry, L.: A generic library for floating-point numbers and its application to exact computing. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 169\u2013184. Springer, Heidelberg (2001). doi:10.1007\/3-540-44755-5_13"},{"issue":"2","key":"22_CR7","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1109\/TC.2010.128","volume":"60","author":"F de Dinechin","year":"2011","unstructured":"de Dinechin, F., Lauter, C., Melquiond, G.: Certifying the floating-point implementation of an elementary function using Gappa. Trans. Comput. 60(2), 242\u2013253 (2011)","journal-title":"Trans. Comput."},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Fumex, C., March\u00e9, C., Moy, Y.: Automated verification of floating-point computations in Ada programs. Research Report RR-9060, Inria Saclay-\u00cele-de-France, April 2017","DOI":"10.1007\/978-3-319-72308-2_7"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45927-8_15","volume-title":"Programming Languages and Systems","author":"E Goubault","year":"2002","unstructured":"Goubault, E., Martel, M., Putot, S.: Asserting the precision of floating-point computations: a simple abstract interpreter. In: M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 209\u2013212. Springer, Heidelberg (2002). doi:10.1007\/3-540-45927-8_15"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"1999","unstructured":"Harrison, J.: A machine-checked theory of floating point arithmetic. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 113\u2013130. Springer, Heidelberg (1999). doi:10.1007\/3-540-48256-3_9"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Leeser, M., Mukherjee, S., Ramachandran, J., Wahl, T.: Make it real: effective floating-point reasoning via exact arithmetic. In: Design, Automation and Test in Europe Conference and Exhibition (DATE), Dresden, Germany, pp. 1\u20134, March 2014","DOI":"10.7873\/DATE2014.130"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/3-540-45578-7_36","volume-title":"Principles and Practice of Constraint Programming \u2014 CP 2001","author":"C Michel","year":"2001","unstructured":"Michel, C., Rueher, M., Lebbah, Y.: Solving constraints over floating-point numbers. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 524\u2013538. Springer, Heidelberg (2001). doi:10.1007\/3-540-45578-7_36"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T00:10:49Z","timestamp":1626135049000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}