{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T11:48:36Z","timestamp":1763466516078},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319085869"},{"type":"electronic","value":"9783319085876"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08587-6_26","type":"book-chapter","created":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T23:38:32Z","timestamp":1404257912000},"page":"344-359","source":"Crossref","is-referenced-by-count":9,"title":["Approximations for Model Construction"],"prefix":"10.1007","author":[{"given":"Aleksandar","family":"Zelji\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph M.","family":"Wintersteiger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-02614-0_10","volume-title":"Intelligent Computer Mathematics","author":"S. Boldo","year":"2009","unstructured":"Boldo, S., Filli\u00e2tre, J.-C., Melquiond, G.: Combining Coq and Gappa for certifying floating-point programs. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) MKM 2009, Held as Part of CICM 2009. LNCS, vol.\u00a05625, pp. 59\u201374. Springer, Heidelberg (2009)"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Brain, M., D\u2019Silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. In: FMSD (2013)","DOI":"10.1007\/s10703-013-0203-7"},{"key":"26_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":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-04772-5_40","volume-title":"Computer Aided Systems Theory - EUROCAST 2009","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Effective bit-width and under-approximation. In: Moreno-D\u00edaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) EUROCAST 2009. LNCS, vol.\u00a05717, pp. 304\u2013311. Springer, Heidelberg (2009)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-540-71209-1_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R.E. Bryant","year":"2007","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.A.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 358\u2013372. Springer, Heidelberg (2007)"},{"key":"26_CR6","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 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 93\u2013107. Springer, Heidelberg (2013)"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Daumas, M., Melquiond, G.: Certification of bounds on expressions involving rounded operators. ACM Trans. Math. Softw.\u00a037(1) (2010)","DOI":"10.1145\/1644001.1644003"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning. In: POPL. ACM (2013)","DOI":"10.1145\/2429069.2429087"},{"key":"26_CR11","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.\u00a07214, pp. 48\u201363. Springer, Heidelberg (2012)"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","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, vol.\u00a07898, pp. 208\u2013214. Springer, Heidelberg (2013)"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y. Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiability modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Giunchiglia, F., Walsh, T.: A theory of abstraction. Artif. Intell. 57(2-3) (1992)","DOI":"10.1016\/0004-3702(92)90021-O"},{"key":"26_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), available on the Web as \n                    \n                      http:\/\/www.cl.cam.ac.uk\/~jrh13\/papers\/tang.html","DOI":"10.1007\/BFb0000475"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511576430"},{"key":"26_CR17","unstructured":"IEEE Comp. Soc.: IEEE Standard for Floating-Point Arithmetic 754-2008 (2008)"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-31612-8_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M. Janota","year":"2012","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 114\u2013128. Springer, Heidelberg (2012)"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Khanh, T.V., Ogawa, M.: SMT for polynomial constraints on real numbers. In: TAPAS. Electronic Notes in Theoretical Computer Science, vol.\u00a0289 (2012)","DOI":"10.1016\/j.entcs.2012.11.004"},{"key":"26_CR20","unstructured":"Lapschies, F., Peleska, J., Gorbachuk, E., Mangels, T.: SONOLAR SMT-solver. In: Satisfiability Modulo Theories Competition; System Description (2012)"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Melquiond, G.: Floating-point arithmetic in the Coq system. In: Conf. on Real Numbers and Computers. Information & Computation, vol.\u00a0216. Elsevier (2012)","DOI":"10.1016\/j.ic.2011.09.005"},{"key":"26_CR22","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.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-36675-8_2","volume-title":"Automated Reasoning and Mathematics","author":"L. Moura de","year":"2013","unstructured":"de Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol.\u00a07788, pp. 15\u201344. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08587-6_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T01:24:01Z","timestamp":1558920241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08587-6_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319085869","9783319085876"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08587-6_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}