{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:50:39Z","timestamp":1780116639575,"version":"3.54.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319942049","type":"print"},{"value":"9783319942056","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94205-6_17","type":"book-chapter","created":{"date-parts":[[2018,6,29]],"date-time":"2018-06-29T12:22:50Z","timestamp":1530274970000},"page":"246-262","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Exploring Approximations for Floating-Point Arithmetic Using UppSAT"],"prefix":"10.1007","author":[{"given":"Aleksandar","family":"Zelji\u0107","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Backeman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph M.","family":"Wintersteiger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,6,30]]},"reference":[{"key":"17_CR1","unstructured":"Bobot, F., Chihani, Z., Marre, B.: Real behavior of floating point. In: 15th International Workshop on Satisfiability Modulo Theories (2017)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-02614-0_10","volume-title":"Intelligent Computer Mathematics","author":"S Boldo","year":"2009","unstructured":"Boldo, S., Filli\u00e2tre, J.-C., Melquiond, G.: Combining Coq and Gappa for certifying floating-point programs. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) CICM 2009. LNCS (LNAI), vol. 5625, pp. 59\u201374. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02614-0_10"},{"key":"17_CR3","first-page":"213","volume":"45","author":"M Brain","year":"2013","unstructured":"Brain, M., D\u2019Silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. FMSD 45, 213\u2013245 (2013)","journal-title":"FMSD"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: FMCAD. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-04772-5_40","volume-title":"Computer Aided Systems Theory - EUROCAST 2009","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Effective bit-width and under-approximation. In: Moreno-D\u00edaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) EUROCAST 2009. LNCS, vol. 5717, pp. 304\u2013311. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-04772-5_40"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-540-71209-1_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"RE Bryant","year":"2007","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 358\u2013372. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71209-1_28"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252. ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"17_CR9","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"Patrick Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Monniaux, D., Rival, X.: The ASTRE\u00c9 analyzer. In: ESOP, Antoine Min\u00e9 (2005)"},{"issue":"1","key":"17_CR10","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/1644001.1644003","volume":"37","author":"M Daumas","year":"2010","unstructured":"Daumas, M., Melquiond, G.: Certification of bounds on expressions involving rounded operators. ACM Trans. Math. Softw. 37(1), 2 (2010)","journal-title":"ACM Trans. Math. Softw."},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"1","key":"17_CR12","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/2480359.2429087","volume":"48","author":"Vijay D'Silva","year":"2013","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning. In: POPL, pp. 143\u2013154. ACM (2013)","journal-title":"ACM SIGPLAN Notices"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-28756-5_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V D\u2019Silva","year":"2012","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric bounds analysis with conflict-driven learning. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 48\u201363. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-28756-5_5"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-319-41540-6_11","volume-title":"Computer Aided Verification","author":"Z Fu","year":"2016","unstructured":"Fu, Z., Su, Z.: XSat: a fast floating-point satisfiability solver. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 187\u2013209. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41540-6_11"},{"key":"17_CR15","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/BFb0000475","volume-title":"Algebraic Methodology and Software Technology","author":"John Harrison","year":"1997","unstructured":"Harrison, J.: Floating point verification in HOL Light: the exponential function. TR 428, University of Cambridge Computer Laboratory (1997)"},{"issue":"3\/4","key":"17_CR16","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1145\/2429135.2429155","volume":"46","author":"D Jovanovic","year":"2012","unstructured":"Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. ACM Comm. Comput. Algebra 46(3\/4), 104\u2013105 (2012)","journal-title":"ACM Comm. Comput. Algebra"},{"key":"17_CR17","unstructured":"Lapschies, F., Peleska, J., Gorbachuk, E., Mangels, T.: SONOLAR SMT-solver. In: SMT-COMP system description (2012)"},{"key":"17_CR18","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/j.ic.2011.09.005","volume":"216","author":"Guillaume Melquiond","year":"2012","unstructured":"Melquiond, G.: Floating-point arithmetic in the Coq system. In: Conference on Real Numbers and Computers, volume 216 of Information & Computation. Elsevier (2012)","journal-title":"Information and Computation"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Ramachandran, J., Wahl, T.: Integrating proxy theories and numeric model lifting for floating-point arithmetic. In: FMCAD. IEEE (2016)","DOI":"10.1109\/FMCAD.2016.7886674"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-319-08587-6_26","volume-title":"Automated Reasoning","author":"A Zelji\u0107","year":"2014","unstructured":"Zelji\u0107, A., Wintersteiger, C.M., R\u00fcmmer, P.: Approximations for model construction. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 344\u2013359. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08587-6_26"},{"issue":"1","key":"17_CR21","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/s10817-016-9393-1","volume":"58","author":"A Zelji\u0107","year":"2017","unstructured":"Zelji\u0107, A., Wintersteiger, C.M., R\u00fcmmer, P.: An approximation framework for solvers and decision procedures. JAR 58(1), 127\u2013147 (2017)","journal-title":"JAR"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94205-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,6,29]],"date-time":"2018-06-29T12:34:23Z","timestamp":1530275663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94205-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319942049","9783319942056"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94205-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}