{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:22:54Z","timestamp":1750220574364,"version":"3.41.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319572871"},{"type":"electronic","value":"9783319572888"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57288-8_16","type":"book-chapter","created":{"date-parts":[[2017,4,8]],"date-time":"2017-04-08T06:45:05Z","timestamp":1491633905000},"page":"230-246","source":"Crossref","is-referenced-by-count":10,"title":["Floating-Point Format Inference in Mixed-Precision"],"prefix":"10.1007","author":[{"given":"Matthieu","family":"Martel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,9]]},"reference":[{"key":"16_CR1","unstructured":"Patriot missile defense: Software problem led to system failure at Dhahran, Saudi Arabia. Technical Report GAO\/IMTEC-92-26, General Accounting office (1992)"},{"key":"16_CR2","unstructured":"ANSI\/IEEE: IEEE Standard for Binary Floating-Point Arithmetic (2008)"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Barr, E.T., Vo, T., Le, V., Su, Z.: Automatic detection of floating-point exceptions. In: POPL 2013, pp. 549\u2013560. ACM (2013)","DOI":"10.1145\/2429069.2429133"},{"key":"16_CR4","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825\u2013885. IOS Press (2009)"},{"issue":"1","key":"16_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1921532.1921553","volume":"36","author":"J Bertrane","year":"2011","unstructured":"Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Static analysis by abstract interpretation of embedded critical software. ACM SIGSOFT Softw. Eng. Notes 36(1), 1\u20138 (2011)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-662-46681-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Phan, A.-D., Fleckenstein, L.: $${\\nu }Z$$ - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194\u2013199. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_14"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Chiang, W., Baranowski, M., Briggs, I., Solovyev, A., Gopalakrishnan, G., Rakamaric, Z.: Rigorous floating-point mixed-precision tuning. In: POPL, pp. 300\u2013315. ACM (2017)","DOI":"10.1145\/3009837.3009846"},{"key":"16_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: Principles of Programming Languages, pp. 238\u2013252. ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR9","unstructured":"Cousot, P., Cousot, R.: A gentle introduction to formal verification of computer systems by abstract interpretation. NATO Science Series III: Computer and Systems Sciences, pp. 1\u201329. IOS Press (2010)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-319-19458-5_3","volume-title":"Formal Methods for Industrial Critical Systems","author":"N Damouche","year":"2015","unstructured":"Damouche, N., Martel, M., Chapoutot, A.: Intra-procedural optimization of the numerical accuracy of programs. In: N\u00fa\u00f1ez, M., G\u00fcdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 31\u201346. Springer, Cham (2015). doi: 10.1007\/978-3-319-19458-5_3"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Darulova, E., Kuncak, V.: Sound compilation of reals. In: Symposium on Principles of Programming Languages, POPL 2014, pp. 235\u2013248. ACM (2014)","DOI":"10.1145\/2535838.2535874"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Gao, X., Bayliss, S., Constantinides, G.A.: SOAP: structural optimization of arithmetic expressions for high-level synthesis. In: International Conference on Field-Programmable Technology, pp. 112\u2013119. IEEE (2013)","DOI":"10.1109\/FPT.2013.6718340"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-38856-9_1","volume-title":"Static Analysis","author":"E Goubault","year":"2013","unstructured":"Goubault, E.: Static analysis by abstract interpretation of numerical programs and systems, and FLUCTUAT. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 1\u20133. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38856-9_1"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-642-18275-4_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Goubault","year":"2011","unstructured":"Goubault, E., Putot, S.: Static analysis of finite precision computations. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 232\u2013247. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-18275-4_17"},{"key":"16_CR15","unstructured":"Halfhill, T.R.: The truth behind the Pentium bug. Byte, March 1995"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Lam, M.O., Hollingsworth, J.K., de Supinski, B.R., LeGendre, M.P.: Automatically adapting programs for mixed-precision floating-point computation. In: Supercomputing, ICS 2013, pp. 369\u2013378. ACM (2013)","DOI":"10.1145\/2464996.2465018"},{"issue":"11","key":"16_CR17","doi-asserted-by":"crossref","first-page":"1925","DOI":"10.1016\/j.cpc.2010.07.006","volume":"181","author":"JL Lamotte","year":"2010","unstructured":"Lamotte, J.L., Chesneaux, J.M., J\u00e9z\u00e9quel, F.: CADNA_C: a version of CADNA for use with C or C++ programs. Comput. Phys. Commu. 181(11), 1925\u20131926 (2010)","journal-title":"Comput. Phys. Commu."},{"issue":"1","key":"16_CR18","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/s10990-006-8608-2","volume":"19","author":"M Martel","year":"2006","unstructured":"Martel, M.: Semantics of roundoff error propagation in finite precision calculations. High.-Order Symb. Comput. 19(1), 7\u201330 (2006)","journal-title":"High.-Order Symb. Comput."},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Martel, M., Najahi, A., Revy, G.: Code size and accuracy-aware synthesis of fixed-point programs for matrix multiplication. In: Pervasive and Embedded Computing and Communication Systems, pp. 204\u2013214. SciTePress (2014)","DOI":"10.5220\/0004884802040214"},{"key":"16_CR20","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.entcs.2012.09.009","volume":"287","author":"A Min\u00e9","year":"2012","unstructured":"Min\u00e9, A.: Inferring sufficient conditions with backward polyhedral under-approximations. Electr. Notes Theor. Comput. Sci. 287, 89\u2013100 (2012)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"16_CR21","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","year":"2008","unstructured":"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). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"16_CR22","unstructured":"Muller, J.M.: On the definition of ulp(x). Technical report 2005\u201309, Laboratoire d\u2019Informatique du Parall\u00e9lisme, Ecole Normale Sup\u00e9rieure de Lyon (2005)"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Muller, J.M., Brisebarre, N., de Dinechin, F., Jeannerod, C.P., Lef\u00e8vre, V., Melquiond, G., Revol, N., Stehl\u00e9, D., Torres, S.: Handbook of Floating-Point Arithmetic. Birkh\u00e4user Boston, Boston (2010)","DOI":"10.1007\/978-0-8176-4705-6"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Nguyen, C., Rubio-Gonzalez, C., Mehne, B., Sen, K., Demmel, J., Kahan, W., Iancu, C., Lavrijsen, W., Bailey, D.H., Hough, D.: Floating-point precision tuning using blame analysis. In: International Conference on Software Engineering (ICSE). ACM (2016)","DOI":"10.1145\/2884781.2884850"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814948_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156\u2013169. Springer, Heidelberg (2006). doi: 10.1007\/11814948_18"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Panchekha, P., Sanchez-Stern, A., Wilcox, J.R., Tatlock, Z.: Automatically improving accuracy for floating point expressions. In: PLDI, pp. 1\u201311. ACM (2015)","DOI":"10.1145\/2737924.2737959"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Rubio-Gonzalez, C., Nguyen, C., Nguyen, H.D., Demmel, J., Kahan, W., Sen, K., Bailey, D.H., Iancu, C., Hough, D.: Precimonious: tuning assistant for floating-point precision. In: International Conference for High Performance Computing, Networking, Storage and Analysis, pp. 27:1\u201327:12. ACM (2013)","DOI":"10.1145\/2503210.2503296"},{"issue":"2","key":"16_CR28","doi-asserted-by":"crossref","first-page":"12:1","DOI":"10.1145\/2699915","volume":"16","author":"R Sebastiani","year":"2015","unstructured":"Sebastiani, R., Tomasi, S.: Optimization modulo theories with linear rational costs. ACM Trans. Comput. Log. 16(2), 12:1\u201312:43 (2015)","journal-title":"ACM Trans. Comput. Log."},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-319-19249-9_33","volume-title":"FM 2015: Formal Methods","author":"A Solovyev","year":"2015","unstructured":"Solovyev, A., Jacobsen, C., Rakamari\u0107, Z., Gopalakrishnan, G.: Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 532\u2013550. Springer, Cham (2015). doi: 10.1007\/978-3-319-19249-9_33"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57288-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:30:33Z","timestamp":1750195833000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57288-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319572871","9783319572888"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57288-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}