{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T04:29:18Z","timestamp":1781756958822,"version":"3.54.5"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030174613","type":"print"},{"value":"9783030174620","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17462-0_5","type":"book-chapter","created":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T01:49:28Z","timestamp":1554342568000},"page":"79-98","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["Building Better Bit-Blasting for Floating-Point Problems"],"prefix":"10.1007","author":[{"given":"Martin","family":"Brain","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Schanda","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Youcheng","family":"Sun","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,4,4]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"IEEE standard for floating-point arithmetic. IEEE Std 754-2008, pp. 1\u201370, August 2008. \n                      https:\/\/doi.org\/10.1109\/IEEESTD.2008.4610935","DOI":"10.1109\/IEEESTD.2008.4610935"},{"key":"5_CR2","unstructured":"AdaCore: CodePeer. \n                      https:\/\/www.adacore.com\/codepeer"},{"key":"5_CR3","unstructured":"Altran, AdaCore: SPARK 2014. \n                      https:\/\/adacore.com\/sparkpro"},{"key":"5_CR4","unstructured":"Bagnara, R., Carlier, M., Gori, R., Gotlieb, A.: Filtering floating-point constraints by maximum ULP (2013). \n                      https:\/\/arxiv.org\/abs\/1308.3847v1"},{"key":"5_CR5","doi-asserted-by":"publisher","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). \n                      https:\/\/doi.org\/10.1145\/2429069.2429133","DOI":"10.1145\/2429069.2429133"},{"key":"5_CR6","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., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"5_CR7","unstructured":"Beyer, D.: SV-COMP. \n                      https:\/\/github.com\/sosy-lab\/sv-benchmarks"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Blanchet, B., et al.: A static analyzer for large safety-critical software. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, PLDI 2003, pp. 196\u2013207. ACM, New York (2003). \n                      https:\/\/doi.org\/10.1145\/781131.781153","DOI":"10.1145\/781131.781153"},{"key":"5_CR9","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53\u201364. Wroclaw, Poland (2011). \n                      https:\/\/hal.inria.fr\/hal-00790310"},{"issue":"4","key":"5_CR10","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1093\/logcom\/exn038","volume":"19","author":"M Brain","year":"2008","unstructured":"Brain, M., De Vos, M.: The significance of memory costs in answer set solver implementation. J. Logic Comput. 19(4), 615\u2013641 (2008). \n                      https:\/\/doi.org\/10.1093\/logcom\/exn038","journal-title":"J. Logic Comput."},{"issue":"2","key":"5_CR11","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10703-013-0203-7","volume":"45","author":"Martin Brain","year":"2013","unstructured":"Brain, M., D\u2019Silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods Syst. Des. 45(2), 213\u2013245 (2014). \n                      https:\/\/doi.org\/10.1007\/s10703-013-0203-7","journal-title":"Formal Methods in System Design"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1007\/978-3-662-49122-5_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Brain","year":"2016","unstructured":"Brain, M., Hadarean, L., Kroening, D., Martins, R.: Automatic generation of propagation complete SAT encodings. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 536\u2013556. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49122-5_26"},{"key":"5_CR13","unstructured":"Brain, M., Tinelli, C.: SMT-LIB floating-point theory, April 2015. \n                      http:\/\/smtlib.cs.uiowa.edu\/theories-FloatingPoint.shtml"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Brain, M., Tinelli, C., R\u00fcmmer, P., Wahl, T.: An automatable formal semantics for IEEE-754, June 2015. \n                      http:\/\/smtlib.cs.uiowa.edu\/papers\/BTRW15.pdf","DOI":"10.1109\/ARITH.2015.26"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: FMCAD, pp. 69\u201376. IEEE (2009). \n                      https:\/\/doi.org\/10.1109\/FMCAD.2009.5351141","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"5_CR16","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"5_CR17","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). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"5_CR18","doi-asserted-by":"publisher","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). \n                      https:\/\/doi.org\/10.1145\/1966445.1966475","DOI":"10.1145\/1966445.1966475"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-319-63390-9_22","volume-title":"Computer Aided Verification","author":"S Conchon","year":"2017","unstructured":"Conchon, S., Iguernlala, M., Ji, K., Melquiond, G., Fumex, C.: A three-tier strategy for reasoning about floating-point numbers in SMT. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 419\u2013435. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63390-9_22"},{"key":"5_CR20","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.) 10th International Workshop on Satisfiability Modulo Theories, pp. 12\u201321. Manchester, United Kingdom, June 2012. \n                      https:\/\/hal.inria.fr\/hal-01785166"},{"key":"5_CR21","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., Martel, M., Panchekha, P., Qiu, C., Sanchez-Stern, A., Tatlock, Z.: 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). \n                      https:\/\/doi.org\/10.1007\/978-3-319-54292-8_6"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Darulova, E., Kuncak, V.: Sound compilation of reals. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 235\u2013248. ACM, New York (2014). \n                      https:\/\/doi.org\/10.1145\/2535838.2535874","DOI":"10.1145\/2535838.2535874"},{"issue":"1","key":"5_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1644001.1644003","volume":"37","author":"Marc Daumas","year":"2010","unstructured":"Daumas, M., Melquiond, G.: Certification of bounds on expressions involving rounded operators. ACM Trans. Math. Softw. 37(1), 2:1\u20132:20 (2010). \n                      https:\/\/doi.org\/10.1145\/1644001.1644003","journal-title":"ACM Transactions on Mathematical Software"},{"key":"5_CR24","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). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Moura de","year":"2013","unstructured":"de Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-35873-9_1"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 143\u2013154. ACM, New York (2013). \n                      https:\/\/doi.org\/10.1145\/2429069.2429087","DOI":"10.1145\/2429069.2429087"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-28756-5_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V D\u2019Silva","year":"2012","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric bounds analysis with conflict-driven learning. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 48\u201363. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-28756-5_5"},{"key":"5_CR28","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). \n                      https:\/\/doi.org\/10.1007\/978-3-319-41540-6_11"},{"key":"5_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175\u2013188. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-27813-9_14"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-38574-2_14"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/11823230_3","volume-title":"Static Analysis","author":"E Goubault","year":"2006","unstructured":"Goubault, E., Putot, S.: Static analysis of numerical algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 18\u201334. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11823230_3"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"680","DOI":"10.1007\/978-3-319-08867-9_45","volume-title":"Computer Aided Verification","author":"L Hadarean","year":"2014","unstructured":"Hadarean, L., Bansal, K., Jovanovi\u0107, D., Barrett, C., Tinelli, C.: A tale of two solvers: eager and lazy approaches to bit-vectors. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 680\u2013695. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-08867-9_45"},{"key":"5_CR33","unstructured":"Hanrot, G., Zimmermann, P., Lef\u00e8vre, V., P\u00e8lissier, P., Th\u00e8veny, P., et al.: The GNU MPFR Library. \n                      http:\/\/www.mpfr.org"},{"key":"5_CR34","unstructured":"Hauser, J.R.: SoftFloat. \n                      http:\/\/www.jhauser.us\/arithmetic\/SoftFloat.html"},{"key":"5_CR35","unstructured":"ISO\/IEC JTC 1\/SC 22\/WG 9 Ada Rapporteur Group: Ada reference manual. ISO\/IEC 8652:2012\/Cor.1:2016 (2016). \n                      http:\/\/www.ada-auth.org\/standards\/rm12_w_tc1\/html\/RM-TOC.html"},{"key":"5_CR36","unstructured":"Izycheva, A., Darulova, E.: On sound relative error bounds for floating-point arithmetic. In: Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017, pp. 15\u201322. FMCAD Inc, Austin, TX (2017). \n                      http:\/\/dl.acm.org\/citation.cfm?id=3168451.3168462"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-31365-3_27"},{"key":"5_CR38","doi-asserted-by":"publisher","unstructured":"Khadra, M.A.B., Stoffel, D., Kunz, W.: goSAT: floating-point satisfiability as global optimization. In: Formal Methods in Computer Aided Design, FMCAD 2017, pp. 11\u201314. IEEE (2017). \n                      https:\/\/doi.org\/10.23919\/FMCAD.2017.8102235","DOI":"10.23919\/FMCAD.2017.8102235"},{"key":"5_CR39","unstructured":"Lapschies, F.: SONOLAR the solver for non-linear arithmetic (2014). \n                      http:\/\/www.informatik.uni-bremen.de\/agbs\/florian\/sonolar"},{"key":"5_CR40","unstructured":"Liew, D.: JFS: JIT fuzzing solver. \n                      https:\/\/github.com\/delcypher\/jfs"},{"key":"5_CR41","doi-asserted-by":"publisher","unstructured":"Liew, D., Schemmel, D., Cadar, C., Donaldson, A.F., Z\u00e4hl, R., Wehrle, K.: Floating-point symbolic execution: a case study in n-version programming, pp. 601\u2013612. IEEE, October 2017. \n                      https:\/\/doi.org\/10.1109\/ASE.2017.8115670","DOI":"10.1109\/ASE.2017.8115670"},{"key":"5_CR42","unstructured":"Marre, B., Bobot, F., Chihani, Z.: Real behavior of floating point numbers. In: SMT Workshop (2017). \n                      http:\/\/smt-workshop.cs.uiowa.edu\/2017\/papers\/SMT2017_paper_21.pdf"},{"key":"5_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/3-540-45578-7_36","volume-title":"Principles and Practice of Constraint Programming \u2014 CP 2001","author":"C Michel","year":"2001","unstructured":"Michel, C., Rueher, M., Lebbah, Y.: Solving constraints over floating-point numbers. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 524\u2013538. Springer, Heidelberg (2001). \n                      https:\/\/doi.org\/10.1007\/3-540-45578-7_36"},{"key":"5_CR44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04267-0","volume-title":"Computer Architecture: Complexity and Correctness","author":"SM Mueller","year":"2000","unstructured":"Mueller, S.M., Paul, W.J.: Computer Architecture: Complexity and Correctness. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/978-3-662-04267-0"},{"key":"5_CR45","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4705-6","volume-title":"Handbook of Floating-Point Arithmetic","author":"Jean-Michel Muller","year":"2010","unstructured":"Muller, J.M., et al.: Handbook of Floating-Point Arithmetic. Birkh\u00e4user (2009). \n                      https:\/\/doi.org\/10.1007\/978-0-8176-4705-6"},{"key":"5_CR46","unstructured":"Neubauer, F., et al.: Accurate dead code detection in embedded C code by arithmetic constraint solving. In: \u00c1brah\u00e1m, E., Davenport, J.H., Fontaine, P. (eds.) Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation. CEUR, vol. 1804, pp. 32\u201338, September 2016. \n                      http:\/\/ceur-ws.org\/Vol-1804\/paper-07.pdf"},{"key":"5_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-642-35873-9_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Pelleau","year":"2013","unstructured":"Pelleau, M., Min\u00e9, A., Truchet, C., Benhamou, F.: A constraint solver based on abstract domains. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 434\u2013454. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-35873-9_26"},{"key":"5_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-642-54013-4_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Romano","year":"2014","unstructured":"Romano, A.: Practical floating-point tests with integer code. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 337\u2013356. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-642-54013-4_19"},{"key":"5_CR49","unstructured":"Schanda, F.: Python arbitrary-precision floating-point library (2017). \n                      https:\/\/www.github.com\/florianschanda\/pympf"},{"key":"5_CR50","unstructured":"Schanda, F., Brain, M., Wintersteiger, C., Griggio, A., et al.: SMT-LIB floating-point benchmarks, June 2017. \n                      https:\/\/github.com\/florianschanda\/smtlib_schanda"},{"key":"5_CR51","unstructured":"Scheibler, K., Kupferschmid, S., Becker, B.: Recent improvements in the SMT solver iSAT. In: Haubelt, C., Timmermann, D. (eds.) Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Warnem\u00fcnde, Germany, pp. 231\u2013241, 12\u201314 March 2013. Institut f\u00fcr Angewandte Mikroelektronik und Datentechnik, Fakult\u00e4t f\u00fcr Informatik und Elektrotechnik, Universit\u00e4t Rostock (2013), \n                      http:\/\/www.avacs.org\/fileadmin\/Publikationen\/Open\/scheibler.mbmv2013.pdf"},{"key":"5_CR52","unstructured":"Scheibler, K., et al.: Accurate ICP-based floating-point reasoning. In: Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design FMCAD 2016, pp. 177\u2013184. FMCAD Inc, Austin, TX (2016). \n                      http:\/\/dl.acm.org\/citation.cfm?id=3077629.3077660"},{"key":"5_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-642-20398-5_26","volume-title":"NASA Formal Methods","author":"M Souza","year":"2011","unstructured":"Souza, M., Borges, M., d\u2019Amorim, M., P\u0103s\u0103reanu, C.S.: CORAL: solving complex constraints for symbolic PathFinder. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 359\u2013374. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-20398-5_26"},{"key":"5_CR54","unstructured":"The MathWorks Inc: Polyspace. \n                      https:\/\/www.mathworks.com\/polyspace"},{"issue":"3","key":"5_CR55","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/s10703-017-0284-9","volume":"51","author":"Vu Xuan Tung","year":"2017","unstructured":"Tung, V.X., Van\u00a0Khanh, T., Ogawa, M.: raSAT: an SMT solver for polynomial constraints. Formal Methods Syst. Des. 51(3), 462\u2013499 (2017). \n                      https:\/\/doi.org\/10.1007\/s10703-017-0284-9","journal-title":"Formal Methods in System Design"},{"key":"5_CR56","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-319-94205-6_17","volume-title":"Automated Reasoning","author":"Aleksandar Zelji\u0107","year":"2018","unstructured":"Zeljic, A., Backeman, P., Wintersteiger, C.M., R\u00fcmmer, P.: Exploring approximations for floating-point arithmetic using UppSAT. In: Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, 14\u201317 July 2018, Proceedings, pp. 246\u2013262 (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-94205-6_17"},{"key":"5_CR57","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-319-08587-6_26","volume-title":"Automated Reasoning","author":"A Zelji\u0107","year":"2014","unstructured":"Zelji\u0107, A., Wintersteiger, C.M., R\u00fcmmer, P.: Approximations for model construction. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 344\u2013359. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-08587-6_26"},{"key":"5_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-319-40970-2_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"A Zelji\u0107","year":"2016","unstructured":"Zelji\u0107, A., Wintersteiger, C.M., R\u00fcmmer, P.: Deciding bit-vector formulas with mcSAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 249\u2013266. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-40970-2_16"},{"key":"5_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"707","DOI":"10.1007\/978-3-319-66158-2_45","volume-title":"Principles and Practice of Constraint Programming","author":"H Zitoun","year":"2017","unstructured":"Zitoun, H., Michel, C., Rueher, M., Michel, L.: Search strategies for floating point constraint\u00a0systems. In: Beck, J.C. (ed.) CP 2017. LNCS, vol. 10416, pp. 707\u2013722. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-66158-2_45"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17462-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T12:06:30Z","timestamp":1570017990000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17462-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030174613","9783030174620"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17462-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"4 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"164","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"42","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"13","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12 full papers and 11 short papers accepted for TOOLympics and SV-COMP (avg. 4 reviewers\/paper, selected from 43 submissions)","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}