{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:10Z","timestamp":1751662870272,"version":"3.37.3"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,11,10]],"date-time":"2016-11-10T00:00:00Z","timestamp":1478736000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100007051","name":"Uppsala University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100007051","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1007\/s10817-016-9393-1","type":"journal-article","created":{"date-parts":[[2016,11,10]],"date-time":"2016-11-10T07:53:11Z","timestamp":1478764391000},"page":"127-147","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["An Approximation Framework for Solvers and Decision Procedures"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0673-9327","authenticated-orcid":false,"given":"Aleksandar","family":"Zelji\u0107","sequence":"first","affiliation":[]},{"given":"Christoph M.","family":"Wintersteiger","sequence":"additional","affiliation":[]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,11,10]]},"reference":[{"key":"9393_CR1","doi-asserted-by":"crossref","unstructured":"Boldo, S., Filli\u00e2tre, J.C., Melquiond, G.: Combining Coq and Gappa for certifying floating-point programs. In: Intelligent Computer Mathematics (Calculemus); MKM\/CICM. LNCS, vol. 5625. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02614-0_10"},{"key":"9393_CR2","unstructured":"Brain, M., D\u2019Silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. FMSD 45(2), 213\u2013245 (2013)"},{"key":"9393_CR3","doi-asserted-by":"crossref","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: FMCAD. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"9393_CR4","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Effective bit-width and under-approximation. In: EUROCAST. LNCS, vol. 5717. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04772-5_40"},{"key":"9393_CR5","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.A.: Deciding bit-vector arithmetic with abstraction. In: TACAS. LNCS, vol. 4424. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-71209-1_28"},{"key":"9393_CR6","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: TACAS. LNCS, vol. 7795. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"9393_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV. LNCS, vol. 1855. Springer, Berlin (2000)","DOI":"10.1007\/10722167_15"},{"key":"9393_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 analyzer. In: ESOP. LNCS, vol. 3444. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"9393_CR9","doi-asserted-by":"publisher","unstructured":"Daumas, M., Melquiond, G.: Certification of bounds on expressions involving rounded operators. ACM Trans. Math. Softw. 37(1) (2010). doi: 10.1145\/1644001.1644003","DOI":"10.1145\/1644001.1644003"},{"key":"9393_CR10","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning. In: POPL. ACM, New York (2013)","DOI":"10.1145\/2429069.2429087"},{"key":"9393_CR11","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric bounds analysis with conflict-driven learning. In: TACAS. LNCS, vol. 7214. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28756-5_5"},{"key":"9393_CR12","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: CADE. LNCS, vol. 7898. Springer, Belin (2013)","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"9393_CR13","doi-asserted-by":"crossref","unstructured":"Ge, Y., de\u00a0Moura, L.: Complete instantiation for quantified formulas in satisfiability modulo theories. In: CAV. LNCS, vol. 5643. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02658-4_25"},{"issue":"2\u20133","key":"9393_CR14","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0004-3702(92)90021-O","volume":"57","author":"F Giunchiglia","year":"1992","unstructured":"Giunchiglia, F., Walsh, T.: A theory of abstraction. Artif. Intell. 57(2\u20133), 323\u2013389 (1992)","journal-title":"Artif. Intell."},{"key":"9393_CR15","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Floating point verification in HOL light: the exponential function. TR 428, University of Cambridge Computer Laboratory (1997)","DOI":"10.1007\/BFb0000475"},{"key":"9393_CR16","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009)"},{"key":"9393_CR17","unstructured":"IEEE Comp. Soc.: IEEE Standard for Floating-Point Arithmetic 754-2008 (2008)"},{"key":"9393_CR18","doi-asserted-by":"crossref","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: SAT. LNCS, vol. 7317. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31612-8_10"},{"key":"9393_CR19","doi-asserted-by":"crossref","unstructured":"Khanh, T.V., Ogawa, M.: SMT for polynomial constraints on real numbers. In: Jeannet, B. (ed.) TAPAS. Electronic Notes in Theoretical Computer Science, vol. 289. Elsevier (2012)","DOI":"10.1016\/j.entcs.2012.11.004"},{"key":"9393_CR20","doi-asserted-by":"crossref","unstructured":"Peleska, J.,Vorobev, E., Lapschies, F.: Automated test case generation with SMT-solving and abstract interpretation. In: NASA formal methods - third international symposium, NFM 2011, Pasadena, CA, USA, April 18\u201320, 2011. Proceedings Springer (2011)","DOI":"10.1007\/978-3-642-20398-5_22"},{"key":"9393_CR21","doi-asserted-by":"crossref","unstructured":"Melquiond, G.: Floating-point arithmetic in the Coq system. In: Conference on Real Numbers and Computers. Information & Computation, vol. 216. Elsevier (2012)","DOI":"10.1016\/j.ic.2011.09.005"},{"key":"9393_CR22","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: TACAS. LNCS, vol. 4963. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9393_CR23","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Automated Reasoning and Mathematics. LNCS, vol. 7788. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-36675-8_2"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9393-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9393-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9393-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,15]],"date-time":"2019-09-15T08:53:52Z","timestamp":1568537632000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9393-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,10]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,1]]}},"alternative-id":["9393"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9393-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2016,11,10]]}}}