{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,7]],"date-time":"2025-03-07T05:13:29Z","timestamp":1741324409633,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214929"},{"type":"electronic","value":"9783642214936"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21493-6_15","type":"book-chapter","created":{"date-parts":[[2011,6,20]],"date-time":"2011-06-20T12:42:44Z","timestamp":1308573764000},"page":"230-246","source":"Crossref","is-referenced-by-count":0,"title":["I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Loup","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability Modulo Theories, ch.\u00a026. Frontiers in Artificial Intelligence and Applications [5], vol.\u00a0185, pp. 825\u2013885 (2009)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"15_CR3","volume-title":"Algorithms in Real Algebraic Geometry","author":"S. Basu","year":"2010","unstructured":"Basu, S., Pollack, R., Roy, M.: Algorithms in Real Algebraic Geometry. Springer, Heidelberg (2010)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Bauer, A., Pister, M., Tautschnig, M.: Tool-support for the analysis of hybrid systems and models. In: DATE 2007, pp. 924\u2013929. European Design and Automation Association (2007)","DOI":"10.1109\/DATE.2007.364411"},{"key":"15_CR5","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","author":"A. Biere","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press, Amsterdam (2009)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-12002-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Bruttomesso","year":"2010","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The openSMT solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 150\u2013153. Springer, Heidelberg (2010)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The mathSAT 4SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 299\u2013303. Springer, Heidelberg (2008)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","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., Moura, L.D.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"issue":"3-4","key":"15_CR10","doi-asserted-by":"crossref","first-page":"209","DOI":"10.3233\/SAT190012","volume":"1","author":"M. Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation\u00a01(3-4), 209\u2013236 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-642-20398-5_41","volume-title":"NASA Formal Methods","author":"U. Loup","year":"2011","unstructured":"Loup, U., \u00c1brah\u00e1m, E.: GiNaCRA: A C++ library for real algebraic computations. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 512\u2013517. Springer, Heidelberg (2011)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: Conflict-Driven Clause Learning SAT Solvers, ch.\u00a04. Frontiers in Artificial Intelligence and Applications [5], vol.\u00a085, pp. 131\u2013153 (2009)","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"15_CR13","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4344-1","volume-title":"Algorithmic Algebra","author":"B. Mishra","year":"1993","unstructured":"Mishra, B.: Algorithmic Algebra. Texts and Monographs in Computer Science. Springer, Heidelberg (1993)"},{"key":"15_CR14","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.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"15_CR15","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.: Solving SAT and SAT modulo theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). Journal of the ACM\u00a053, 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"15_CR16","unstructured":"SMT competition 2010, http:\/\/www.smtcomp.org\/2010\/"},{"issue":"2","key":"15_CR17","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002000050055","volume":"8","author":"V. Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra \u2013 The quadratic case and beyond. Applicable Algebra in Engineering, Communication and Computing\u00a08(2), 85\u2013101 (1997)","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","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.: Satisfiability of non-linear (Ir)rational\u00a0arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 481\u2013500. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Algebraic Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21493-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,6]],"date-time":"2025-03-06T11:43:42Z","timestamp":1741261422000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21493-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214929","9783642214936"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21493-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}