{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T18:44:55Z","timestamp":1771958695377,"version":"3.50.1"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319955810","type":"print"},{"value":"9783319955827","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-95582-7_21","type":"book-chapter","created":{"date-parts":[[2018,7,11]],"date-time":"2018-07-11T10:31:17Z","timestamp":1531305077000},"page":"355-363","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Combining Tools for Optimization and Analysis of Floating-Point Computations"],"prefix":"10.1007","author":[{"given":"Heiko","family":"Becker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavel","family":"Panchekha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eva","family":"Darulova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zachary","family":"Tatlock","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,12]]},"reference":[{"key":"21_CR1","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) International Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Becker, H., Panchekha, P., Darulova, E., Tatlock, Z.: Combining tools for optimization and analysis of floating-point computations. arXiv preprint arXiv:1805.02436 (2018)","DOI":"10.1007\/978-3-319-95582-7_21"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Chiang, W.F., Baranowski, M., Briggs, I., Solovyev, A., Gopalakrishnan, G., Rakamari\u0107, Z.: Rigorous floating-point mixed-precision tuning. In: Symposium on Principles of Programming Languages (POPL), pp. 300\u2013315. ACM (2017)","DOI":"10.1145\/3093333.3009846"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Chiang, W.F., Gopalakrishnan, G., Rakamaric, Z., Solovyev, A.: Efficient search for inputs causing high floating-point errors. In: Symposium on Principles and Practice of Parallel Programming (PPoPP), vol. 49, pp. 43\u201352. ACM (2014)","DOI":"10.1145\/2555243.2555265"},{"key":"21_CR5","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). https:\/\/doi.org\/10.1007\/978-3-319-19458-5_3"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-319-54292-8_6","volume-title":"Numerical Software Verification","author":"N Damouche","year":"2017","unstructured":"Damouche, N., et al.: Toward a standard benchmark format and suite for floating-point analysis. In: Bogomolov, S., Martel, M., Prabhakar, P. (eds.) NSV 2016. LNCS, vol. 10152, pp. 63\u201377. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-54292-8_6"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Darulova, E., Horn, E., Sharma, S.: Sound mixed-precision optimization with rewriting. In: International Conference on Cyber-Physical Systems (ICCPS) (2018)","DOI":"10.1109\/ICCPS.2018.00028"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-319-89960-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Darulova","year":"2018","unstructured":"Darulova, E., et al.: Daisy - framework for analysis and optimization of numerical programs (tool paper). In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 270\u2013287. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_15"},{"issue":"2","key":"21_CR9","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/3014426","volume":"39","author":"E Darulova","year":"2017","unstructured":"Darulova, E., Kuncak, V.: Towards a compiler for reals. ACM Trans. Program. Lang. Syst. (TOPLAS) 39(2), 8 (2017)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"De Dinechin, F., Lauter, C.Q., Melquiond, G.: Assisted verification of elementary functions using Gappa. In: ACM Symposium on Applied Computing, pp. 1318\u20131322. ACM (2006)","DOI":"10.1145\/1141277.1141584"},{"key":"21_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). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24 . http:\/\/dl.acm.org\/citation.cfm?id=1792734.1792766"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-03542-0_4","volume-title":"Programming Languages and Systems","author":"E Goubault","year":"2013","unstructured":"Goubault, E., Putot, S.: Robustness analysis of finite precision implementations. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 50\u201357. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03542-0_4"},{"key":"21_CR13","unstructured":"IEEE Computer Society: IEEE standard for floating-point arithmetic. IEEE Std 754\u20132008 (2008)"},{"issue":"7","key":"21_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"4","key":"21_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3015465","volume":"43","author":"V Magron","year":"2017","unstructured":"Magron, V., Constantinides, G., Donaldson, A.: Certified roundoff error bounds using semidefinite programming. ACM Trans. Math. Softw. 43(4), 1\u201334 (2017)","journal-title":"ACM Trans. Math. Softw."},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-319-66266-4_14","volume-title":"Computer Safety, Reliability, and Security","author":"M Moscato","year":"2017","unstructured":"Moscato, M., Titolo, L., Dutle, A., Mu\u00f1oz, C.A.: Automatic estimation of verified floating-point round-off errors via static analysis. In: Tonetta, S., Schoitsch, E., Bitsch, F. (eds.) SAFECOMP 2017. LNCS, vol. 10488, pp. 213\u2013229. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66266-4_14"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Panchekha, P., Sanchez-Stern, A., Wilcox, J.R., Tatlock, Z.: Automatically improving accuracy for floating point expressions. In: Conference on Programming Language Design and Implementation (PLDI) (2015)","DOI":"10.1145\/2737924.2737959"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Ramananandro, T., Mountcastle, P., Meister, B., Lethin, R.: A unified Coq framework for verifying C programs with floating-point computations. In: Certified Programs and Proofs (CPP), pp. 15\u201326. ACM (2016)","DOI":"10.1145\/2854065.2854066"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Rubio-Gonz\u00e1lez, 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: Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis, SC 2013, pp. 27:1\u201327:12. ACM (2013)","DOI":"10.1145\/2503210.2503296"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Sanchez-Stern, A., Panchekha, P., Lerner, S., Tatlock, Z.: Finding root causes of floating point error with herbgrind. arXiv preprint arXiv:1705.10416 (2017)","DOI":"10.1145\/3192366.3192411"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Schkufza, E., Sharma, R., Aiken, A.: Stochastic optimization of floating-point programs with tunable precision. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 53\u201364. ACM (2014)","DOI":"10.1145\/2666356.2594302"},{"key":"21_CR22","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). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_33"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Zou, D., Wang, R., Xiong, Y., Zhang, L., Su, Z., Mei, H.: A genetic algorithm for detecting significant floating-point inaccuracies. In: IEEE International Conference on Software Engineering (ICSE), vol. 1, pp. 529\u2013539. IEEE (2015)","DOI":"10.1109\/ICSE.2015.70"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-95582-7_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T12:29:56Z","timestamp":1571574596000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-95582-7_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319955810","9783319955827"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-95582-7_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}