{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:56:08Z","timestamp":1743119768153,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319708478"},{"type":"electronic","value":"9783319708485"}],"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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-70848-5_7","type":"book-chapter","created":{"date-parts":[[2017,11,10]],"date-time":"2017-11-10T10:43:26Z","timestamp":1510310606000},"page":"91-106","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Encoding Floating-Point Numbers Using the SMT Theory in ESBMC: An Empirical Evaluation over the SV-COMP Benchmarks"],"prefix":"10.1007","author":[{"given":"Mikhail Y. R.","family":"Gadelha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lucas C.","family":"Cordeiro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Denis A.","family":"Nicole","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,11]]},"reference":[{"issue":"8","key":"7_CR1","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1109\/TC.1982.1676076","volume":"C\u201331","author":"GW Gerrity","year":"1982","unstructured":"Gerrity, G.W.: Computer representation of real numbers. IEEE Trans. Comput. C\u201331(8), 709\u2013714 (1982)","journal-title":"IEEE Trans. Comput."},{"key":"7_CR2","unstructured":"Frantz, G., Simar, R.: Comparing fixed- and floating-point DSPs. SPRY061, Texas Instruments (2004)"},{"key":"7_CR3","unstructured":"IEEE: IEEE standard for floating-point arithmetic. Technical report, August 2008"},{"issue":"1","key":"7_CR4","doi-asserted-by":"crossref","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 Comput. Surv. 23(1), 5\u201348 (1991)","journal-title":"ACM Comput. Surv."},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Nikoli\u0107, Z., Nguyen, H.T., Frantz, G.: Design and implementation of numerical linear algebra algorithms on fixed point DSPs. EURASIP J. Adv. Sig. Proc. 2007(1) (2007)","DOI":"10.1155\/2007\/87046"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Cordeiro, L.C., Fischer, B.: Verifying multi-threaded software using SMT-based context-bounded model checking. In: ICSE, pp. 331\u2013340 (2011)","DOI":"10.1145\/1985793.1985839"},{"issue":"4","key":"7_CR7","doi-asserted-by":"crossref","first-page":"957","DOI":"10.1109\/TSE.2011.59","volume":"38","author":"LC Cordeiro","year":"2012","unstructured":"Cordeiro, L.C., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. IEEE Trans. Softw. Eng. 38(4), 957\u2013974 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"7_CR8","unstructured":"R\u00fcmmer, P., Wahl, T.: An SMT-lib theory of binary floating-point arithmetic. In: SMT Workshop (2010)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-23404-5_9","volume-title":"Model Checking Software","author":"HI Ismail","year":"2015","unstructured":"Ismail, H.I., Bessa, I.V., Cordeiro, L.C., Lima Filho, E.B., Chaves Filho, J.E.: DSVerifier: a bounded model checking tool for digital systems. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 126\u2013131. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23404-5_9"},{"issue":"1","key":"7_CR10","doi-asserted-by":"crossref","first-page":"1:1","DOI":"10.1186\/s13173-016-0041-8","volume":"22","author":"RB Abreu","year":"2016","unstructured":"Abreu, R.B., Gadelha, M.Y.R., Cordeiro, L.C., Filho, E.B.D.L., de Silva Jr., W.S.: Bounded model checking for fixed-point digital filters. J. Braz. Comput. Soc. 22(1), 1:1\u20131:20 (2016)","journal-title":"J. Braz. Comput. Soc."},{"issue":"2","key":"7_CR11","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/s10617-016-9173-5","volume":"20","author":"I Bessa","year":"2016","unstructured":"Bessa, I., Ismail, H., Cordeiro, L.C., Filho, J.E.C.: Verification of fixed-point digital controllers using direct and delta forms realizations. Des. Autom. Embed. Syst. 20(2), 95\u2013126 (2016)","journal-title":"Des. Autom. Embed. Syst."},{"issue":"3","key":"7_CR12","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1109\/TC.2016.2601328","volume":"66","author":"I Bessa","year":"2017","unstructured":"Bessa, I., Ismail, H., Palhares, R., Cordeiro, L.C., Filho, J.E.C.: Formal non-fragile stability verification of digital control systems with uncertainty. IEEE Trans. Comput. 66(3), 545\u2013552 (2017)","journal-title":"IEEE Trans. Comput."},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-662-54580-5_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2017","unstructured":"Beyer, D.: Software verification with validation of results. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 331\u2013349. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_20"},{"key":"7_CR14","unstructured":"Wang, D., Zhang, C., Chen, G., Gu, M., Sun, J.G.: C code verification based on the extended labeled transition system model. In: D&P@MoDELS, pp. 48\u201355 (2016)"},{"key":"7_CR15","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). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Ramalho, M., Freitas, M., Sousa, F., Marques, H., Cordeiro, L.C., Fischer, B.: SMT-based bounded model checking of C++ programs. In: ECBS, pp. 147\u2013156 (2013)","DOI":"10.1109\/ECBS.2013.15"},{"issue":"1","key":"7_CR17","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/s10009-015-0407-9","volume":"19","author":"MYR Gadelha","year":"2017","unstructured":"Gadelha, M.Y.R., Ismail, H.I., Cordeiro, L.C.: Handling loops in bounded model checking of C programs via k-induction. STTT 19(1), 97\u2013114 (2017)","journal-title":"STTT"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: An efficient method of computing static single assignment form. In: POPL, pp. 25\u201335 (1989)","DOI":"10.1145\/75277.75280"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174\u2013177. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_16"},{"key":"7_CR20","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"},{"key":"7_CR21","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). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Brain, M., Tinelli, C., Ruemmer, P., Wahl, T.: An automatable formal semantics for IEEE-754 floating-point arithmetic. In: ARITH, pp. 160\u2013167 (2015)","DOI":"10.1109\/ARITH.2015.26"},{"key":"7_CR25","unstructured":"Smith, R.: Working Draft, Standard for Programming Language C++ (2016). Accessed Jan 2017"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-04570-7_6","volume-title":"Formal Methods for Industrial Critical Systems","author":"D Delmas","year":"2009","unstructured":"Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., V\u00e9drine, F.: Towards an industrial use of FLUCTUAT on safety-critical avionics software. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 53\u201369. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04570-7_6"},{"issue":"7","key":"7_CR27","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-14295-6_11","volume-title":"Computer Aided Verification","author":"T Ball","year":"2010","unstructured":"Ball, T., Bounimova, E., Levin, V., Kumar, R., Lichtenberg, J.: The static driver verifier research platform. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 119\u2013122. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_11"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-662-48288-9_9","volume-title":"Static Analysis","author":"M Brain","year":"2015","unstructured":"Brain, M., Joshi, S., Kroening, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 145\u2013161. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48288-9_9"},{"key":"7_CR30","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). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_11"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70848-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,5]],"date-time":"2019-10-05T20:36:56Z","timestamp":1570307816000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70848-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319708478","9783319708485"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70848-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}