{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T11:10:09Z","timestamp":1746097809966,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642540127"},{"type":"electronic","value":"9783642540134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54013-4_19","type":"book-chapter","created":{"date-parts":[[2014,1,3]],"date-time":"2014-01-03T01:08:09Z","timestamp":1388711289000},"page":"337-356","source":"Crossref","is-referenced-by-count":5,"title":["Practical Floating-Point Tests with Integer Code"],"prefix":"10.1007","author":[{"given":"Anthony","family":"Romano","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-642-24372-1_3","volume-title":"Automated Technology for Verification and Analysis","author":"J. Alglave","year":"2011","unstructured":"Alglave, J., Donaldson, A.F., Kroening, D., Tautschnig, M.: Making software verification tools really work. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 28\u201342. Springer, Heidelberg (2011)"},{"key":"19_CR2","first-page":"10","volume-title":"Proceedings of the 6th IEEE International Conference on Software Testing, Verification and Validation","author":"R. Bagnara","year":"2013","unstructured":"Bagnara, R., Carlier, M., Gori, R., Gotlieb, A.: Symbolic path-oriented test data generation for floating-point programs. In: Proceedings of the 6th IEEE International Conference on Software Testing, Verification and Validation, p. 10. IEEE Press, Luxembourg City (2013)"},{"key":"19_CR3","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1145\/2429069.2429133","volume-title":"Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013","author":"E.T. Barr","year":"2013","unstructured":"Barr, E.T., Vo, T., Le, V., Su, Z.: Automatic detection of floating-point exceptions. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 549\u2013560. ACM, New York (2013)"},{"key":"19_CR4","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/781131.781153","volume-title":"Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLD 2003)","author":"B. Blanchet","year":"2003","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLD 2003), June 7-14, pp. 196\u2013207. ACM Press, San Diego (2003)"},{"issue":"2","key":"19_CR5","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1002\/stvr.333","volume":"16","author":"B. Botella","year":"2006","unstructured":"Botella, B., Gotlieb, A., Michel, C.: Symbolic execution of floating-point computations. Software Testing, Verification and Reliability\u00a016(2), 97\u2013121 (2006)","journal-title":"Software Testing, Verification and Reliability"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: FMCAD, pp. 69\u201376. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-22110-1_37","volume-title":"Computer Aided Verification","author":"D. Brumley","year":"2011","unstructured":"Brumley, D., Jager, I., Avgerinos, T., Schwartz, E.J.: BAP: A binary analysis platform. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 463\u2013469. Springer, Heidelberg (2011)"},{"key":"19_CR8","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI 2008, pp. 209\u2013224 (2008)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Chipounov, V., Kuznetsov, V., Candea, G.: S2E: a platform for in-vivo multi-path analysis of software systems. In: ASPLOS 2011, pp. 265\u2013278 (2011)","DOI":"10.1145\/1961295.1950396"},{"issue":"5","key":"19_CR10","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"19_CR11","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1145\/1966445.1966475","volume-title":"Proceedings of the Sixth Conference on Computer Systems, EuroSys 2011","author":"P. Collingbourne","year":"2011","unstructured":"Collingbourne, P., Cadar, C., Kelly, P.H.: Symbolic crosschecking of floating-point and SIMD code. In: Proceedings of the Sixth Conference on Computer Systems, EuroSys 2011, pp. 315\u2013328. ACM, New York (2011)"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Conchon, S., Melquiond, G., Roux, C., Iguernelala, M.: Built-in treatment of an axiomatic floating-point theory for SMT solvers. In: Fontaine, P., Goel, A. (eds.) SMT 2012. EPiC Series, vol.\u00a020, pp. 12\u201321. Easy Chair (2013)","DOI":"10.29007\/wh99"},{"key":"19_CR13","first-page":"238","volume-title":"Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1977","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1977, pp. 238\u2013252. ACM, New York (1977)"},{"issue":"3","key":"19_CR14","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/0004-3702(87)90091-9","volume":"32","author":"E. Davis","year":"1987","unstructured":"Davis, E.: Constraint propagation with interval labels. Artificial Intelligence\u00a032(3), 281\u2013331 (1987)","journal-title":"Artificial Intelligence"},{"key":"19_CR15","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.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"19_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1831708.1831710","volume-title":"Proceedings of the 19th International Symposium on Software Testing and Analysis, ISSTA 2010","author":"P. Godefroid","year":"2010","unstructured":"Godefroid, P., Kinder, J.: Proving memory safety of floating-point computations by combining static and dynamic program analysis. In: Proceedings of the 19th International Symposium on Software Testing and Analysis, ISSTA 2010, pp. 1\u201312. ACM, New York (2010)"},{"key":"19_CR18","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Network Distributed Security Symposium (2008)"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Taly, A.: Automated synthesis of symbolic instruction encodings from I\/O samples. In: PLDI, pp. 441\u2013452 (2012)","DOI":"10.1145\/2345156.2254116"},{"key":"19_CR20","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/103162.103163","volume":"23","author":"D. Goldberg","year":"1991","unstructured":"Goldberg, D.: What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys\u00a023, 5\u201348 (1991)","journal-title":"ACM Computing Surveys"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/11823230_3","volume-title":"Static Analysis","author":"\u00c9. Goubault","year":"2006","unstructured":"Goubault, \u00c9., Putot, S.: Static analysis of numerical algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 18\u201334. Springer, Heidelberg (2006)"},{"key":"19_CR22","unstructured":"Haller, L., Griggio, A., Brain, M., Kroening, D.: Deciding floating-point logic with systematic abstraction. In: Cabodi, G., Singh, S. (eds.) FMCAD, pp. 131\u2013140. IEEE (2012)"},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-04694-0_6","volume-title":"Runtime Verification","author":"T. Hansen","year":"2009","unstructured":"Hansen, T., Schachte, P., S\u00f8ndergaard, H.: State joining and splitting for the symbolic execution of binaries. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol.\u00a05779, pp. 76\u201392. Springer, Heidelberg (2009)"},{"key":"19_CR24","unstructured":"Hauser, J.: SoftFloat-2b (2002), http:\/\/www.jhauser.us\/arithmetic\/SoftFloat.html"},{"key":"19_CR25","unstructured":"IEEE Task P754: ANSI\/IEEE 754-1985, Standard for Binary Floating-Point Arithmetic (August 1985)"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Ivan\u010dic\u0300, F., Ganai, M.K., Sankaranarayanan, S., Gupta, A.: Software model checking the precision of floating-point programs. In: Proceedings of the 8th ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), pp. 49\u201358. IEEE (2010)","DOI":"10.1109\/MEMCOD.2010.5558622"},{"key":"19_CR27","unstructured":"Kahan, W.: Implementation of algorithms (lecture notes by W. S. Haugeland and D. Hough). Technical Report\u00a020 (1973)"},{"key":"19_CR28","unstructured":"Karrer, J.: Softgun \u2013 the embedded system simulator (2013), http:\/\/softgun.sourceforge.net"},{"key":"19_CR29","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Communications of the ACM\u00a019, 385\u2013394 (1976)","journal-title":"Communications of the ACM"},{"issue":"3","key":"19_CR30","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1134\/S036176880703005X","volume":"33","author":"V.V. Kuliamin","year":"2007","unstructured":"Kuliamin, V.V.: Standardization and testing of implementations of mathematical functions in floating point numbers. Programming and Computer Software\u00a033(3), 154\u2013173 (2007)","journal-title":"Programming and Computer Software"},{"key":"19_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-16573-3_11","volume-title":"Testing Software and Systems","author":"K. Lakhotia","year":"2010","unstructured":"Lakhotia, K., Tillmann, N., Harman, M., de Halleux, J.: FloPSy - search-based floating point constraint solving for symbolic execution. In: Petrenko, A., Sim\u00e3o, A., Maldonado, J.C. (eds.) ICTSS 2010. LNCS, vol.\u00a06435, pp. 142\u2013157. Springer, Heidelberg (2010)"},{"key":"19_CR32","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/2145816.2145844","volume-title":"Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2012","author":"G. Li","year":"2012","unstructured":"Li, G., Li, P., Sawaya, G., Gopalakrishnan, G., Ghosh, I., Rajan, S.P.: GKLEE: concolic verification and test generation for GPUs. In: Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2012, pp. 215\u2013224. ACM, New York (2012)"},{"key":"19_CR33","first-page":"337","volume-title":"ASPLOS 2012","author":"L. Martignoni","year":"2012","unstructured":"Martignoni, L., McCamant, S., Poosankam, P., Song, D., Maniatis, P.: Path-exploration lifting: hi-fi tests for lo-fi emulators. In: ASPLOS 2012, pp. 337\u2013348. ACM, New York (2012)"},{"key":"19_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-24725-8_2","volume-title":"Programming Languages and Systems","author":"A. Min\u00e9","year":"2004","unstructured":"Min\u00e9, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D.A. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 3\u201317. Springer, Heidelberg (2004)"},{"key":"19_CR35","unstructured":"Molnar, D., Li, X.C., Wagner, D.A.: Dynamic test generation to find integer bugs in x86 binary linux programs. In: Proceedings of the 18th Conference on USENIX Security Symposium, SSYM 2009, pp. 67\u201382. USENIX Association (2009)"},{"issue":"3","key":"19_CR36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1353445.1353446","volume":"30","author":"D. Monniaux","year":"2008","unstructured":"Monniaux, D.: The pitfalls of verifying floating-point computations. ACM Trans. Program. Lang. Syst.\u00a030(3), 12:1\u201312:41 (2008)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"19_CR37","doi-asserted-by":"crossref","unstructured":"Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. In: PLDI 2007, pp. 89\u2013100 (2007)","DOI":"10.1145\/1250734.1250746"},{"key":"19_CR38","unstructured":"O\u2019Leary, J., Zhao, X., Gerth, R., Seger, C.J.H.: Formally verifying IEEE compliance of floating-point hardware. Tech. rep., Intel Technical Journal (First quarter 1999)"},{"key":"19_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-20398-5_22","volume-title":"NASA Formal Methods","author":"J. Peleska","year":"2011","unstructured":"Peleska, J., Vorobev, E., Lapschies, F.: Automated test case generation with SMT-solving and abstract interpretation. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 298\u2013312. Springer, Heidelberg (2011)"},{"key":"19_CR40","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/s10009-009-0118-1","volume":"11","author":"C. P\u0103s\u0103reanu","year":"2009","unstructured":"P\u0103s\u0103reanu, C., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. International Journal on Software Tools for Technology Transfer (STTT)\u00a011, 339\u2013353 (2009)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"19_CR41","unstructured":"R\u00fcmmer, P.: Preliminary SMT-FPA conformance tests (2010), http:\/\/www.cprover.org\/SMT-LIB-Float\/"},{"key":"19_CR42","unstructured":"R\u00fcmmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: Informal Proceedings of 8th International Workshop on Satisfiability Modulo Theories (SMT) at FLoC, Edinburgh, Scotland (2010)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54013-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T10:40:08Z","timestamp":1746096008000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54013-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642540127","9783642540134"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54013-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}