{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:16:18Z","timestamp":1759637778175,"version":"3.37.3"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,4,20]],"date-time":"2016-04-20T00:00:00Z","timestamp":1461110400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,4,20]],"date-time":"2016-04-20T00:00:00Z","timestamp":1461110400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-C-0284"],"award-info":[{"award-number":["FA8750-12-C-0284"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1423298"],"award-info":[{"award-number":["CNS-1423298"]}],"id":[{"id":"10.13039\/100000001","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":[[2016,6]]},"DOI":"10.1007\/s10703-016-0245-8","type":"journal-article","created":{"date-parts":[[2016,4,20]],"date-time":"2016-04-20T07:46:30Z","timestamp":1461138390000},"page":"257-273","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A search-based procedure for nonlinear real arithmetic"],"prefix":"10.1007","volume":"48","author":[{"given":"Ashish","family":"Tiwari","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Lincoln","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,4,20]]},"reference":[{"issue":"3","key":"245_CR1","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour B, Paulson LC (2010) MetiTarski: An automatic theorem prover for real-valued special functions. J Autom Reason 44(3):175\u2013205","journal-title":"J Autom Reason"},{"key":"245_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair L, Ganzinger H (1994) Buchberger\u2019s algorithm: a constraint-based completion procedure. In: Proceedings of 1st international conference constraints in computational logic, LNCS 845, Springer, pp 285\u2013301","DOI":"10.1007\/BFb0016860"},{"issue":"6","key":"245_CR3","doi-asserted-by":"publisher","first-page":"1002","DOI":"10.1145\/235809.235813","volume":"43","author":"S Basu","year":"1996","unstructured":"Basu S, Pollack R, Roy MF (1996) On the combinatorial and algebraic complexity of quantifier elimination. J ACM 43(6):1002\u20131045","journal-title":"J ACM"},{"key":"245_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03718-8","volume-title":"Real algebraic geometry","author":"J Bochnak","year":"1998","unstructured":"Bochnak J, Coste M, Roy MF (1998) Real algebraic geometry. Springer, New York"},{"key":"245_CR5","doi-asserted-by":"crossref","unstructured":"Buchberger B (1983) A critical-pair completion algorithm for finitely generated ideals in rings. In: Proceedings of logic and machines: decision problems and complexity, LNCS, vol. 171, pp 137\u2013161","DOI":"10.1007\/3-540-13331-3_39"},{"key":"245_CR6","doi-asserted-by":"crossref","unstructured":"Cheng CH, Ruess H, Shankar N (2013) JBernstein: a validity checker for generalized polynomial constraints. In: Proceedings of 25th international conference computer aided verification, CAV, vol. LNCS 8044, Springer, pp 656\u2013661","DOI":"10.1007\/978-3-642-39799-8_43"},{"key":"245_CR7","unstructured":"Cheng CH, Shankar N, Ruess H, Bensalem S (2013) EFSMT: a logical framework for cyber-physical systems. CoRR abs\/1306.3456"},{"key":"245_CR8","unstructured":"Collins GE (1975) Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: Proceedings of 2nd GI Conference on Automata Theory and Formal Languages, LNCS, Springer, vol. 33, pp 134\u2013183"},{"issue":"3","key":"245_CR9","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"GE Collins","year":"1991","unstructured":"Collins GE, Hong H (1991) Partial cylindrical algebraic decomposition for quantifier elimination. J Symb Comput 12(3):299\u2013328","journal-title":"J Symb Comput"},{"key":"245_CR10","doi-asserted-by":"crossref","unstructured":"Colon M, Sankaranarayanan S, Sipma H (2003) Linear invariant generation using non-linear constraint solving. In: Computer-Aided Verification (CAV), LNCS, Springer-Verlag, vol. 2725, pp 420\u2013433","DOI":"10.1007\/978-3-540-45069-6_39"},{"issue":"1\u20132","key":"245_CR11","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\u20132):29\u201335","journal-title":"J Symb Comput"},{"issue":"7","key":"245_CR12","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis M, Logemann G, Loveland D (1962) A machine program for theorem-proving. CACM 5(7):394\u2013397","journal-title":"CACM"},{"key":"245_CR13","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s00211-007-0114-x","volume":"108","author":"J Demmel","year":"2007","unstructured":"Demmel J, Dumitriu I, Holtz O (2007) Fast linear algebra is stable. Numer Math 108:59\u201391","journal-title":"Numer Math"},{"issue":"3\u20134","key":"245_CR14","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. JSAT 1(3\u20134):209\u2013236","journal-title":"JSAT"},{"key":"245_CR15","doi-asserted-by":"crossref","unstructured":"Ganzinger H, Hagen G, Nieuwenhuis R, Oliveras A, Tinelli C (2004) DPLL(T): fast decision procedures. In: Proceedings of 16th International Conference on Computer Aided Verification, CAV 2004, LNCS, Springer, vol 3114, pp 175\u2013188","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"245_CR16","unstructured":"Gao S, Avigad J, Clarke EM (2012) $$\\delta $$-complete decisionprocedures for satisfiability over the reals. In: Proceedings 6th International Conference Automated Reasoning, IJCAR, LNCS 7364, pp 286\u2013300"},{"key":"245_CR17","doi-asserted-by":"crossref","unstructured":"Gao S, Kong S, Clarke EM (2013) dReal: An SMT solver for nonlinear theories over the reals. In: Proceedings of 24th International Conference on Automated Deduction, CADE, LNCS 7898, Springer, pp 208\u2013214","DOI":"10.1007\/978-3-642-38574-2_14"},{"issue":"1\u20132","key":"245_CR18","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0747-7171(88)80006-3","volume":"5","author":"D Grigoriev","year":"1988","unstructured":"Grigoriev D (1988) Complexity of deciding Tarski algebra. J Symb Comput 5(1\u20132):65\u2013108","journal-title":"J Symb Comput"},{"key":"245_CR19","doi-asserted-by":"crossref","unstructured":"Gulwani S, Jha S, Tiwari A, Venkatesan R (2011) Synthesis of loop-free programs. In: Proceedings of ACM Conference on Prgramming Language Designing and Implementation of PLDI, pp 62\u201373","DOI":"10.1145\/1993498.1993506"},{"key":"245_CR20","doi-asserted-by":"crossref","unstructured":"Gulwani S, Srivastava S, Venkatesan R (2008) Program analysis as constraint solving. In: Proceedings of ACM Conference on Prgramming Language Design and implementaion, PLDI, pp 281\u2013292","DOI":"10.1145\/1375581.1375616"},{"key":"245_CR21","doi-asserted-by":"crossref","unstructured":"Gulwani S, Tiwari A (2008) Constraint-based approach for analysis of hybrid systems. In: Proceedings of 20th International Conference on Computer Aided Verification, CAV 2008, LNCS, vol. 5123, pp 190\u2013203. Springer. July 7\u201314, 2008, Princeton, NJ","DOI":"10.1007\/978-3-540-70545-1_18"},{"key":"245_CR22","doi-asserted-by":"crossref","unstructured":"Hong H (1990) An improvement of the projection operator in cylindrical algebraic decomposition. In: Proceedings of ISAAC 90, pp 261\u2013264","DOI":"10.1145\/96877.96943"},{"key":"245_CR23","doi-asserted-by":"publisher","unstructured":"Hong H, Safey El Din M (2009) Variant real quantifier elimination: algorithm and application. In: ISSAC, pp 183\u2013190. ACM. doi:\n                    10.1145\/1576702.1576729","DOI":"10.1145\/1576702.1576729"},{"key":"245_CR24","doi-asserted-by":"crossref","unstructured":"Iwane H, Yanami H, Anai H (2011) An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for optimization problems. In: Proceedings of International Workshop on Symbolic Numeric Computation, SNC, pp 168\u2013177. ACM","DOI":"10.1145\/2331684.2331712"},{"key":"245_CR25","doi-asserted-by":"crossref","unstructured":"Jovanovic D, de Moura LM (2012) Solving non-linear arithmetic. In: Proceedings of 6th International Conference Automated Reasoning, IJCAR, LNCS 7364, Springer, pp 339\u2013354","DOI":"10.1007\/978-3-642-31365-3_27"},{"key":"245_CR26","doi-asserted-by":"crossref","unstructured":"Leike J (2014) Software and benchmarks for synthesis for polynomial lasso programs \n                    http:\/\/www.csl.sri.com\/~tiwari\/softwares\/synthesis_for_polynomial_lasso_programs_source.zip","DOI":"10.1007\/978-3-642-54013-4_24"},{"key":"245_CR27","doi-asserted-by":"crossref","unstructured":"Leike J, Tiwari A (2014) Synthesis for polynomial lasso programs. In: Proceedings of VMCAI, LNCS 8318, pp 454\u2013472","DOI":"10.1007\/978-3-642-54013-4_24"},{"key":"245_CR28","doi-asserted-by":"crossref","unstructured":"Loup U, Scheibler K, Corzilius F, \u00c1brah\u00e1m E, Becker B (2013) A symbiosis of interval constraint propagation and cylindrical algebraic decomposition. In: Proceedings of 24th International Conference on Automated Deduction, CADE, LNCS 7898, Springer, pp 193\u2013207","DOI":"10.1007\/978-3-642-38574-2_13"},{"key":"245_CR29","unstructured":"Matringe N, Moura AV, Rebiha R (2010) Generating invariants for non-linear hybrid systems by linear algebraic methods. In: Proceedings of 17th International Static Analysis Symposium, SAS, Springer, vol. LNCS 6337, pp 373\u2013389"},{"key":"245_CR30","unstructured":"Microsoft Research: Z3: An efficient SMT solver. \n                    http:\/\/research.microsoft.com\/projects\/z3\/"},{"issue":"2","key":"245_CR31","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"PA Parrilo","year":"2003","unstructured":"Parrilo PA (2003) Semidefinite programming relaxations for semialgebraic problems. Math Program Ser B 96(2):293\u2013320","journal-title":"Math Program Ser B"},{"key":"245_CR32","doi-asserted-by":"crossref","unstructured":"Rebiha R, Matringe N, Moura AV (2012) Transcendental inductive invariants generation for non-linear differential and hybrid systems. In: Proceedings of Hybrid System: Computation and Control, HSCC, pp 25\u201334. ACM","DOI":"10.1145\/2185632.2185640"},{"issue":"3","key":"245_CR33","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/S0747-7171(10)80003-3","volume":"13","author":"J Renegar","year":"1992","unstructured":"Renegar J (1992) On the computational complexity and geometry of the first-order theory of the reals. J Symb Comput 13(3):255\u2013352","journal-title":"J Symb Comput"},{"key":"245_CR34","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S, Sipma H, Manna Z (2004) Constructing invariants for hybrid systems. In: R. Alur, G.J. Pappas (eds.) Hybrid systems: computation and control, HSCC 2004, Lecture Notes in Computer Science, vol. 2993, pp 539\u2013554. Springer","DOI":"10.1007\/978-3-540-24743-2_36"},{"issue":"1","key":"245_CR35","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10703-007-0046-1","volume":"32","author":"S Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan S, Sipma HB, Manna Z (2008) Constructing invariants for hybrid systems. Formal Methods Syst Des 32(1):25\u201355","journal-title":"Formal Methods Syst Des"},{"key":"245_CR36","unstructured":"SRI International: Yices: An SMT solver. \n                    http:\/\/yices.csl.sri.com\/"},{"issue":"5\u20136","key":"245_CR37","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/s10009-012-0223-4","volume":"15","author":"S Srivastava","year":"2013","unstructured":"Srivastava S, Gulwani S, Foster JS (2013) Template-based program verification and program synthesis. STTT 15(5\u20136):497\u2013518","journal-title":"STTT"},{"key":"245_CR38","unstructured":"Stengle G (1974) A Nullstellensatz and a Positivstellensatz insemialgebraic geometry. Math Ann 207"},{"key":"245_CR39","doi-asserted-by":"crossref","unstructured":"Sturm T, Tiwari A (2011) Verification and synthesis using real quantifier elimination. In: Proceedings of International Symposium on Symbolic and Algebraic Computation , ISSAC, pp 329\u2013336. ACM","DOI":"10.1145\/1993886.1993935"},{"key":"245_CR40","doi-asserted-by":"crossref","unstructured":"Taly A, Gulwani S, Tiwari A (2009) Synthesizing switching logic using constraint solving. In: Proc. 10th Intl. Conf. on Verification, Model Checking and Abstract Interpretation, VMCAI, LNCS, Springer, vol. 5403, pp 305\u2013319","DOI":"10.1007\/978-3-540-93900-9_25"},{"key":"245_CR41","volume-title":"A decision method for elementary algebra and geometry","author":"A Tarski","year":"1948","unstructured":"Tarski A (1948) A decision method for elementary algebra and geometry, 2nd edn. University of California Press, Berkeley","edition":"2"},{"key":"245_CR42","doi-asserted-by":"crossref","unstructured":"Tiwari A (2005) An algebraic approach for the unsatisfiability of nonlinear constraints. In: Computer Science Logic, 14th Annual Conference, CSL 2005, LNCS, Springer, vol. 3634, pp 248\u2013262","DOI":"10.1007\/11538363_18"},{"key":"245_CR43","doi-asserted-by":"crossref","unstructured":"Tiwari A, Khanna G (2004) Nonlinear Systems: Approximating reach sets. In: Proceedings of 7th International Workshop on Hybrid Systems: Computation and Control, HSCC 2004, LNCS, Springer, vol. 2993, pp 600\u2013614","DOI":"10.1007\/978-3-540-24743-2_40"},{"key":"245_CR44","doi-asserted-by":"crossref","unstructured":"Tiwari A, Lincoln P (2014) A nonlinear real arithmetic fragment. In: Proceedings on Computer Aided Verification CAV, LNCS, Springer, vol. 8559, pp 729\u2013736","DOI":"10.1007\/978-3-319-08867-9_48"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0245-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-016-0245-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0245-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0245-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T15:42:46Z","timestamp":1589730166000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-016-0245-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,20]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["245"],"URL":"https:\/\/doi.org\/10.1007\/s10703-016-0245-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2016,4,20]]},"assertion":[{"value":"20 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}