{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T00:10:43Z","timestamp":1777421443432,"version":"3.51.4"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319542911","type":"print"},{"value":"9783319542928","type":"electronic"}],"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-54292-8_6","type":"book-chapter","created":{"date-parts":[[2017,2,16]],"date-time":"2017-02-16T02:12:49Z","timestamp":1487211169000},"page":"63-77","source":"Crossref","is-referenced-by-count":43,"title":["Toward a Standard Benchmark Format and Suite for Floating-Point Analysis"],"prefix":"10.1007","author":[{"given":"Nasrine","family":"Damouche","sequence":"first","affiliation":[]},{"given":"Matthieu","family":"Martel","sequence":"additional","affiliation":[]},{"given":"Pavel","family":"Panchekha","sequence":"additional","affiliation":[]},{"given":"Chen","family":"Qiu","sequence":"additional","affiliation":[]},{"given":"Alexander","family":"Sanchez-Stern","sequence":"additional","affiliation":[]},{"given":"Zachary","family":"Tatlock","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,2,17]]},"reference":[{"key":"6_CR1","unstructured":"DIMACS challenge. Satisfiability. Suggested format (1993). http:\/\/www.cs.ubc.ca\/~hoos\/SATLIB\/Benchmarks\/SAT\/satformat.ps"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-319-26529-2_8","volume-title":"Programming Languages and Systems","author":"A Adj\u00e9","year":"2015","unstructured":"Adj\u00e9, A., Garoche, P.-L., Werey, A.: Quadratic zonotopes. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 127\u2013145. Springer, Cham (2015). doi: 10.1007\/978-3-319-26529-2_8"},{"key":"6_CR3","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). www.SMT-LIB.org"},{"issue":"2\u20133","key":"6_CR4","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1561\/2500000002","volume":"2","author":"J Bertrane","year":"2015","unstructured":"Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Static analysis and verification of aerospace software by abstract interpretation. Found. Trends Program. Lang. 2(2\u20133), 71\u2013190 (2015)","journal-title":"Found. Trends Program. Lang."},{"issue":"2","key":"6_CR5","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1145\/1646353.1646374","volume":"53","author":"A Bessey","year":"2010","unstructured":"Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., Engler, D.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53(2), 66\u201375 (2010)","journal-title":"Commun. ACM"},{"key":"6_CR6","unstructured":"Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI 2008), Berkeley, CA, USA, pp. 209\u2013224. USENIX Association (2008)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-15769-1_12","volume-title":"Static Analysis","author":"A Chapoutot","year":"2010","unstructured":"Chapoutot, A.: Interval slopes as a numerical abstract domain for floating-point variables. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 184\u2013200. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15769-1_12"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24730-2_15"},{"issue":"4","key":"6_CR9","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Log. Comput. 2(4), 511\u2013547 (1992)","journal-title":"J. Log. Comput."},{"key":"6_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":"6_CR11","doi-asserted-by":"crossref","unstructured":"Darulova, E., Kuncak, V.: Sound compilation of reals. In: Jagannathan, S., Sewell, P., (eds.), POPL 2014, pp. 235\u2013248. ACM (2014)","DOI":"10.1145\/2535838.2535874"},{"key":"6_CR12","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":"6_CR13","unstructured":"Goubault, E., Martel, M., Putot, S.: Some future challenges in the validation of control systems. In: European Congress on Embedded Real Time Software (ERTS 2006), Proceedings (2006)"},{"key":"6_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":"6_CR15","doi-asserted-by":"crossref","unstructured":"Griewank, A., Walther, A.: Evaluating derivatives - principles and techniques of algorithmic differentiation (2 ed.). SIAM (2008)","DOI":"10.1137\/1.9780898717761"},{"key":"6_CR16","volume-title":"Numerical Methods for Scientists and Engineers","author":"R Hamming","year":"1987","unstructured":"Hamming, R.: Numerical Methods for Scientists and Engineers, 2nd edn. Dover Publications, New York (1987)","edition":"2"},{"issue":"4","key":"6_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1186736.1186737","volume":"34","author":"JL Henning","year":"2006","unstructured":"Henning, J.L.: SPEC CPU2006 benchmark descriptions. SIGARCH Comput. Archit. News 34(4), 1\u201317 (2006)","journal-title":"SIGARCH Comput. Archit. News"},{"issue":"2","key":"6_CR18","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1145\/2560217.2560218","volume":"57","author":"GJ Holzmann","year":"2014","unstructured":"Holzmann, G.J.: Mars code. Commun. ACM 57(2), 64\u201373 (2014)","journal-title":"Commun. ACM"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Lee, W., Sharma, R., Aiken, A.: Verifying bit-manipulations of floating-point. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2016), New York, NY, USA. ACM (2016)","DOI":"10.1145\/2908080.2908107"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-540-30579-8_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Martel","year":"2005","unstructured":"Martel, M.: An overview of semantics for the validation of numerical programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 59\u201377. Springer, Heidelberg (2005). doi: 10.1007\/978-3-540-30579-8_4"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Wilcox, J.-R., Panchekha, P., Sanchez-Stern, A., Tatlock, Z.: Automatically improving accuracy for floating point expressions. In: Grove, D., Blackburn, S., (eds.), PLDI 2015, pp. 1\u201311. ACM (2015)","DOI":"10.1145\/2813885.2737959"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-38856-9_2","volume-title":"Static Analysis","author":"S Sankaranarayanan","year":"2013","unstructured":"Sankaranarayanan, S.: Static analysis in the continuously changing world. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 4\u20135. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38856-9_2"},{"key":"6_CR23","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), New York, NY, USA. ACM (2014)","DOI":"10.1145\/2666356.2594302"},{"key":"6_CR24","series-title":"Programming and Software Engineering","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: Formal Methods. Programming and Software Engineering, vol. 9109. Springer, Heidelberg (2015)"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Woo, S.C., Ohara, M., Torrie, E., Singh, J.P., Gupta, A.: The SPLASH-2 programs: characterization and methodological considerations. In: Proceedings of the 22nd Annual International Symposium on Computer Architecture (ISCA 1995), pp. 24\u201336, New York, NY, USA. ACM (1995)","DOI":"10.1145\/223982.223990"}],"container-title":["Lecture Notes in Computer Science","Numerical Software Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-54292-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,18]],"date-time":"2019-09-18T15:03:23Z","timestamp":1568819003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-54292-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319542911","9783319542928"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-54292-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}