{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T03:41:14Z","timestamp":1769744474789,"version":"3.49.0"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,6,27]],"date-time":"2017-06-27T00:00:00Z","timestamp":1498521600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,6,27]],"date-time":"2017-06-27T00:00:00Z","timestamp":1498521600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["23300005"],"award-info":[{"award-number":["23300005"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["15H02684"],"award-info":[{"award-number":["15H02684"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1007\/s10703-017-0284-9","type":"journal-article","created":{"date-parts":[[2017,6,27]],"date-time":"2017-06-27T09:12:53Z","timestamp":1498554773000},"page":"462-499","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["raSAT: an SMT solver for polynomial constraints"],"prefix":"10.1007","volume":"51","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2239-6574","authenticated-orcid":false,"given":"Vu Xuan","family":"Tung","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"To","family":"Van Khanh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mizuhito","family":"Ogawa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,6,27]]},"reference":[{"key":"284_CR1","unstructured":"Alliot JM, Gotteland JB, Vanaret C, Durand N, Gianazza D (2012) Implementing an interval computation library for OCaml on x86\/amd64 architectures. In: OUD 2012, OCaml users and developers workshop"},{"key":"284_CR2","doi-asserted-by":"crossref","unstructured":"Barr ET, Vo T, Le V, Su Z (2013) Automatic detection of floating-point exceptions. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, ACM, New York, POPL \u201913, pp 549\u2013560","DOI":"10.1145\/2429069.2429133"},{"key":"284_CR3","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1016\/S1574-6526(06)80020-9","volume-title":"Handbook of constraint programming","author":"F Benhamou","year":"2006","unstructured":"Benhamou F, Granvilliers L (2006) Continuous and interval constraints. In: Rossi F, Pv B, Walsh T (eds) Handbook of constraint programming. Elsevier, New York, pp 571\u2013604"},{"key":"284_CR4","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-70545-1_27","volume-title":"Computer aided verification","author":"M Bofill","year":"2008","unstructured":"Bofill M, Nieuwenhuis R, Oliveras A, Rodr\u00edguez-Carbonell E, Rubio A (2008) The barcelogic SMT solver. In: Gupta A, Malik S (eds) Computer aided verification. Springer, Berlin, pp 294\u2013298"},{"key":"284_CR5","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10703-013-0203-7","volume":"45","author":"M Brain","year":"2014","unstructured":"Brain M, D\u2019Silva V, Griggio A, Haller L, Kroening D (2014) Deciding floating-point logic with abstract conflict driven clause learning. Form Methods Syst Des 45:213\u2013245","journal-title":"Form Methods Syst Des"},{"key":"284_CR6","unstructured":"Comba JLD, Stolfi J (1993) Affine arithmetic and its applications to computer graphics. In: SIBGRAPI\u201993, pp 9\u201318"},{"issue":"1","key":"284_CR7","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"JH Davenport","year":"1988","unstructured":"Davenport JH, Heintz J (1988) Real quantifier elimination is doubly exponential. J Symb Comput 5(1):29\u201335","journal-title":"J Symb Comput"},{"key":"284_CR8","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 (2012) Numeric bounds analysis with conflict-driven learning. In: Flanagan C, K\u00f6nig B (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 48\u201363"},{"key":"284_CR9","doi-asserted-by":"crossref","unstructured":"D\u2019Silva V, Haller L, Kroening D (2013) Abstract conflict driven learning. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, ACM, New York, POPL \u201913, pp 143\u2013154","DOI":"10.1145\/2429069.2429087"},{"key":"284_CR10","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer aided verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre B, de Moura L (2006) A fast linear-arithmetic solver for DPLL(T). In: Ball T, Jones RB (eds) Computer aided verification. Springer, Berlin, pp 81\u201394"},{"key":"284_CR11","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and applications of satisfiability testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n N, S\u00f6rensson N (2004) An extensible SAT-solver. In: Giunchiglia E, Tacchella A (eds) Theory and applications of satisfiability testing. Springer, Berlin, pp 502\u2013518"},{"key":"284_CR12","first-page":"442","volume-title":"Theory and applications of satisfiability testing\u2013SAT 2012","author":"C Florian","year":"2012","unstructured":"Florian C, Ulrich L, Sebastian J, Erika \u00c1 (2012) SMT-RAT: an SMT-compliant nonlinear real arithmetic toolbox. In: Alessandro C, Roberto S (eds) Theory and applications of satisfiability testing\u2013SAT 2012. Springer, Berlin, pp 442\u2013448"},{"key":"284_CR13","first-page":"209","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle M, Herde C, Teige T, Ratschan S, Schubert T (2007) Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J Satisf Boolean Model Comput 1:209\u2013236","journal-title":"J Satisf Boolean Model Comput"},{"key":"284_CR14","unstructured":"Ganai M, Ivancic F (2009) Efficient decision procedure for non-linear arithmetic constraints using cordic. In: Formal methods in computer-aided design, 2009. FMCAD 2009, pp 61\u201368"},{"key":"284_CR15","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated deduction\u2013CADE-24","author":"S Gao","year":"2013","unstructured":"Gao S, Kong S, Clarke E (2013a) dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina M (ed) Automated deduction\u2013CADE-24. Springer, Berlin, pp 208\u2013214"},{"key":"284_CR16","first-page":"105","volume":"2013","author":"S Gao","year":"2013","unstructured":"Gao S, Kong S, Clarke EM (2013) Satisfiability modulo ODEs. Form Methods Comput Aided Des (FMCAD) 2013:105\u2013112","journal-title":"Form Methods Comput Aided Des (FMCAD)"},{"key":"284_CR17","doi-asserted-by":"crossref","unstructured":"Goldsztejn A (2006) A branch and prune algorithm for the approximation of non-linear ae-solution sets. In: Proceedings of the 2006 ACM symposium on applied computing, ACM, New York, USA, pp 1650\u20131654","DOI":"10.1145\/1141277.1141665"},{"key":"284_CR18","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1145\/1132973.1132980","volume":"32","author":"L Granvilliers","year":"2006","unstructured":"Granvilliers L, Benhamou F (2006) RealPaver: an interval solver using constraint satisfaction techniques. ACM Trans Math Softw 32:138\u2013156","journal-title":"ACM Trans Math Softw"},{"key":"284_CR19","unstructured":"Haller L, Griggio A, Brain M, Kroening D (2012) Deciding floating-point logic with systematic abstraction. In: 2012 formal methods in computer-aided design (FMCAD), pp 131\u2013140"},{"key":"284_CR20","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/s10601-012-9126-y","volume":"17","author":"D Ishii","year":"2012","unstructured":"Ishii D, Goldsztejn A, Jermann C (2012) Interval-based projection method for under-constrained numerical systems. Constraints 17:432\u2013460","journal-title":"Constraints"},{"key":"284_CR21","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 (2012) Solving non-linear arithmetic. In: Gramlich B, Miller D, Sattler U (eds) Automated reasoning. Springer, Berlin, pp 339\u2013354"},{"key":"284_CR22","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.entcs.2012.11.004","volume":"289","author":"TV Khanh","year":"2012","unstructured":"Khanh TV, Ogawa M (2012) SMT for polynomial constraints on real numbers. Electron Notes Theor Comput Sci 289:27\u201340 (third Workshop on Tools for Automatic Program Analysis (TAPAS\u2019 2012))","journal-title":"Electron Notes Theor Comput Sci"},{"key":"284_CR23","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-38574-2_13","volume-title":"Automated deduction\u2013CADE-24","author":"U Loup","year":"2013","unstructured":"Loup U, Scheibler K, Corzilius F, \u00c1brah\u00e1m E, Becker B (2013) A symbiosis of interval constraint propagation and cylindrical algebraic decomposition. In: Bonacina MP (ed) Automated deduction\u2013CADE-24. Springer, Berlin, pp 193\u2013207"},{"key":"284_CR24","first-page":"992","volume":"8","author":"F Messine","year":"2002","unstructured":"Messine F (2002) Extentions of affine arithmetic: application to unconstrained global optimization. J Univers Comput Sci 8:992\u20131015","journal-title":"J Univers Comput Sci"},{"key":"284_CR25","first-page":"2192","volume":"E86\u2013A","author":"S Miyajima","year":"2003","unstructured":"Miyajima S, Miyata T, Kashiwagi M (2003) A new dividing method in affine arithmetic. IEICE Trans Fundam Electron Commun Comput Sci E86\u2013A:2192\u20132196","journal-title":"IEICE Trans Fundam Electron Commun Comput Sci"},{"key":"284_CR26","volume-title":"Interval analysis","author":"R Moore","year":"1966","unstructured":"Moore R (1966) Interval analysis. Prentice-Hall, Englewood Cliffs"},{"key":"284_CR27","volume-title":"Interval methods for systems of equations","author":"A Neumaier","year":"1990","unstructured":"Neumaier A (1990) Interval methods for systems of equations. Cambridge University Press, Cambridge"},{"key":"284_CR28","unstructured":"Ngoc DTB, Ogawa M (2009) Overflow and roundoff error analysis via model checking. In: Proceedings of the 2009 seventh IEEE international conference on software engineering and formal methods, IEEE computer society, Washington, SEFM \u201909, pp 105\u2013114"},{"key":"284_CR29","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J ACM 53:937\u2013977","journal-title":"J ACM"},{"key":"284_CR30","unstructured":"Passmore GO (2011) Combined decision procedures for nonlinear arithmetics, real and complex. Dissertation, School of informatics, University of Edinburgh"},{"key":"284_CR31","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-02614-0_14","volume-title":"Intelligent computer mathematics","author":"GO Passmore","year":"2009","unstructured":"Passmore GO, Jackson PB (2009) Combined decision techniques for the existential theory of the reals. In: Carette J, Dixon L, Coen CS, Watt SM (eds) Intelligent computer mathematics. Springer, Berlin, pp 122\u2013137"},{"key":"284_CR32","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1145\/1183278.1183282","volume":"7","author":"S Ratschan","year":"2006","unstructured":"Ratschan S (2006) Efficient solving of quantified inequality constraints over the real numbers. ACM Trans Comput Log 7:723\u2013748","journal-title":"ACM Trans Comput Log"},{"key":"284_CR33","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1016\/S0021-9800(69)80045-1","volume":"7","author":"B Rennie","year":"1969","unstructured":"Rennie B, Dobson A (1969) On stirling numbers of the second kind. J Comb Theory 7:116\u2013121","journal-title":"J Comb Theory"},{"key":"284_CR34","unstructured":"Stolfi J, Figueiredo LHD (1997) Self-validated numerical methods and applications. In: Monograph for 21st Brazilian mathematics colloquium"},{"key":"284_CR35","doi-asserted-by":"crossref","unstructured":"Sturm T (2015) Subtropical real root finding. In: Proceedings of the 2015 ACM on international symposium on symbolic and algebraic computation, ACM, New York, ISSAC \u201915, pp 347\u2013354","DOI":"10.1145\/2755996.2756677"},{"key":"284_CR36","volume-title":"Automation of reasoning, symbolic computation","author":"G Tseitin","year":"1983","unstructured":"Tseitin G (1983) On the complexity of derivation in propositional calculus. In: Siekmann JH, Wrightson G (eds) Automation of reasoning, symbolic computation. Springer, Berlin"},{"key":"284_CR37","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/978-3-319-40229-1_16","volume-title":"Automated reasoning","author":"VX Tung","year":"2016","unstructured":"Tung VX, Van Khanh T, Ogawa M (2016) raSAT: an SMT solver for polynomial constraints. In: Olivetti N, Tiwari A (eds) Automated reasoning. Springer, Cham, pp 228\u2013237"},{"key":"284_CR38","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-642-17511-4_27","volume-title":"Logic for programming, artificial intelligence, and reasoning","author":"H Zankl","year":"2010","unstructured":"Zankl H, Middeldorp A (2010) Satisfiability of non-linear (ir)rational arithmetic. In: Clarke EM, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning. Springer, Berlin, pp 481\u2013500"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0284-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0284-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0284-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T15:46:42Z","timestamp":1589730402000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0284-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,27]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["284"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0284-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,6,27]]},"assertion":[{"value":"27 June 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}