{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:29:53Z","timestamp":1759638593455,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319712369"},{"type":"electronic","value":"9783319712376"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-71237-6_24","type":"book-chapter","created":{"date-parts":[[2017,11,17]],"date-time":"2017-11-17T20:13:02Z","timestamp":1510949582000},"page":"491-513","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Sharper and Simpler Nonlinear Interpolants for Program Verification"],"prefix":"10.1007","author":[{"given":"Takamasa","family":"Okudono","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuki","family":"Nishida","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kensuke","family":"Kojima","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kohei","family":"Suenaga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kengo","family":"Kido","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,19]]},"reference":[{"key":"24_CR1","unstructured":"Anai, H., Parrilo, P.A.: Convex quantifier elimination for semidefinite programming. In: Proceedings of the International Workshop on Computer Algebra in Scientific Computing, CASC (2003)"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-74464-1_4","volume-title":"Types for Proofs and Programs","author":"F Besson","year":"2007","unstructured":"Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48\u201362. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-74464-1_4"},{"key":"24_CR3","volume-title":"Real Algebraic Geometry","author":"J Bochnak","year":"1999","unstructured":"Bochnak, J., Coste, M., Roy, M.F.: Real Algebraic Geometry. Springer, New York (1999)"},{"issue":"5","key":"24_CR4","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003). \n                      https:\/\/doi.org\/10.1145\/876638.876643","journal-title":"J. ACM"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., Somenzi [14], pp. 420\u2013432","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"24_CR6","unstructured":"Dai, L.: The tool \n                      \n                        \n                      \n                      $$\\mathtt{{aiSat}}$$\n                      \n                        \n                          aiSat\n                        \n                      \n                    . \n                      github.com\/djuanbei\/aiSat\n                      \n                    . Accessed 17 Jan 2017"},{"key":"24_CR7","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1016\/j.jsc.2016.07.010","volume":"80","author":"L Dai","year":"2017","unstructured":"Dai, L., Gan, T., Xia, B., Zhan, N.: Barrier certificates revisited. J. Symb. Comput. 80, 62\u201386 (2017). \n                      https:\/\/doi.org\/10.1016\/j.jsc.2016.07.010","journal-title":"J. Symb. Comput."},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-39799-8_25","volume-title":"Computer Aided Verification","author":"L Dai","year":"2013","unstructured":"Dai, L., Xia, B., Zhan, N.: Generating non-linear interpolants by semidefinite programming. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 364\u2013380. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-39799-8_25"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-319-40229-1_14","volume-title":"Automated Reasoning","author":"T Gan","year":"2016","unstructured":"Gan, T., Dai, L., Xia, B., Zhan, N., Kapur, D., Chen, M.: Interpolant synthesis for quadratic polynomial inequalities and combination with EUF. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 195\u2013212. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-40229-1_14"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-662-49674-9_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Gao","year":"2016","unstructured":"Gao, S., Zufferey, D.: Interpolants in nonlinear theories over the reals. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 625\u2013641. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49674-9_41"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-02444-8_19","volume-title":"Automated Technology for Verification and Analysis","author":"A Gurfinkel","year":"2013","unstructured":"Gurfinkel, A., Rollini, S.F., Sharygina, N.: Interpolation properties and SAT-based model checking. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 255\u2013271. Springer, Cham (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-319-02444-8_19"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-74591-4_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2007","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 102\u2013118. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-74591-4_9"},{"key":"24_CR13","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14\u201316, 2004. pp. 232\u2013244. ACM (2004). \n                      http:\/\/dl.acm.org\/citation.cfm?id=964001"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/b11831","volume-title":"Computer Aided Verification","year":"2003","unstructured":"Hunt Jr., W.A., Somenzi, F. (eds.): CAV 2003. LNCS, vol. 2725. Springer, Heidelberg (2003). \n                      https:\/\/doi.org\/10.1007\/b11831"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/11513988_6","volume-title":"Computer Aided Verification","author":"R Jhala","year":"2005","unstructured":"Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 39\u201351. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11513988_6"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459\u2013473. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11691372_33"},{"key":"24_CR17","unstructured":"Kaltofen, E., Li, B., Yang, Z., Zhi, L.: Exact certification of global optimality of approximate factorizations via rationalizing sums-of-squares with floating point scalars. In: Sendra, J.R., Gonz\u00e1lez-Vega, L. (eds.) Symbolic and Algebraic Computation, International Symposium, ISSAC 2008, Linz\/Hagenberg, Austria, July 20\u201323, 2008, Proceedings, pp. 155\u2013164. ACM (2008). \n                      http:\/\/doi.acm.org\/10.1145\/1390768.1390792"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-642-24310-3_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Kupferschmid","year":"2011","unstructured":"Kupferschmid, S., Becker, B.: Craig interpolation in the presence of non-linear constraints. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 240\u2013255. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-24310-3_17"},{"key":"24_CR19","series-title":"Springer Books on Elementary mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4220-8","volume-title":"Introduction to Diophantine Approximations","author":"S Lang","year":"1995","unstructured":"Lang, S.: Introduction to Diophantine Approximations. Springer Books on Elementary mathematics. Springer, New York (1995). \n                      https:\/\/doi.org\/10.1007\/978-1-4612-4220-8"},{"issue":"2","key":"24_CR20","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/s11704-014-3150-6","volume":"8","author":"W Lin","year":"2014","unstructured":"Lin, W., Wu, M., Yang, Z., Zeng, Z.: Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods. Front. Comput. Sci. 8(2), 192\u2013202 (2014). \n                      https:\/\/doi.org\/10.1007\/s11704-014-3150-6","journal-title":"Front. Comput. Sci."},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Interpolation and sat-based model checking. In: Hunt Jr., Somenzi [14], pp. 1\u201313","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1\u201312. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/978-3-540-31980-1_1"},{"key":"24_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11817963_14"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Okudono, T., Nishida, Y., Kojima, K., Suenaga, K., Kido, K., Hasuo, I.: Sharper and simpler nonlinear interpolants for program verification. CoRR abs\/1709.00314 (2017)","DOI":"10.1007\/978-3-319-71237-6_24"},{"key":"24_CR25","unstructured":"Parrilo, P.: Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. Ph.D. thesis, California Inst. of Tech. (2000)"},{"issue":"2","key":"24_CR26","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"PA Parrilo","year":"2003","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293\u2013320 (2003). \n                      https:\/\/doi.org\/10.1007\/s10107-003-0387-5","journal-title":"Math. Program."},{"issue":"2","key":"24_CR27","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.tcs.2008.09.025","volume":"409","author":"H Peyrl","year":"2008","unstructured":"Peyrl, H., Parrilo, P.A.: Computing sum of squares decompositions with rational coefficients. Theor. Comput. Sci. 409(2), 269\u2013281 (2008). \n                      https:\/\/doi.org\/10.1016\/j.tcs.2008.09.025","journal-title":"Theor. Comput. Sci."},{"key":"24_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-642-02959-2_35","volume-title":"Automated Deduction \u2013 CADE-22","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.-D., R\u00fcmmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 485\u2013501. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-02959-2_35"},{"issue":"3","key":"24_CR29","doi-asserted-by":"publisher","first-page":"969","DOI":"10.1512\/iumj.1993.42.42045","volume":"42","author":"M Putinar","year":"1993","unstructured":"Putinar, M.: Positive polynomials on compact semi-algebraic sets. Indiana Univ. Math. Journ. 42(3), 969\u2013984 (1993)","journal-title":"Indiana Univ. Math. Journ."},{"key":"24_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-662-53413-7_21","volume-title":"Static Analysis","author":"P Roux","year":"2016","unstructured":"Roux, P., Voronin, Y.-L., Sankaranarayanan, S.: Validating numerical semidefinite programming solvers for polynomial invariants. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 424\u2013446. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-53413-7_21"},{"issue":"2","key":"24_CR31","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s10543-006-0056-1","volume":"46","author":"S Rump","year":"2006","unstructured":"Rump, S.: Verification of positive definiteness. BIT Numer. Math. 46(2), 433\u2013452 (2006). \n                      https:\/\/doi.org\/10.1007\/s10543-006-0056-1","journal-title":"BIT Numer. Math."},{"key":"24_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-69738-1_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Rybalchenko","year":"2007","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346\u2013362. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-69738-1_25"},{"key":"24_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/978-3-642-37036-6_31","volume-title":"Programming Languages and Systems","author":"R Sharma","year":"2013","unstructured":"Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 574\u2013592. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-37036-6_31"},{"issue":"2","key":"24_CR34","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/BF01362149","volume":"207","author":"G Stengle","year":"1974","unstructured":"Stengle, G.: A Nullstellensatz and a Positivstellensatz in semialgebraic geometry. Math. Ann. 207(2), 87\u201397 (1974). \n                      https:\/\/doi.org\/10.1007\/BF01362149","journal-title":"Math. Ann."},{"key":"24_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-662-48288-9_8","volume-title":"Static Analysis","author":"T Terauchi","year":"2015","unstructured":"Terauchi, T.: Explaining the effectiveness of small refinement heuristics in program verification with CEGAR. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 128\u2013144. Springer, Heidelberg (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-662-48288-9_8"},{"key":"24_CR36","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1080\/10556789908805762","volume":"11","author":"KC Toh","year":"1999","unstructured":"Toh, K.C., Todd, M., T\u00fct\u00fcnc\u00fc, R.H.: Sdpt3 - a matlab software package for semidefinite programming. Optim. Methods Softw. 11, 545\u2013581 (1999)","journal-title":"Optim. Methods Softw."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-71237-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T02:59:00Z","timestamp":1558321140000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-71237-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319712369","9783319712376"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-71237-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"19 November 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Suzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 November 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 November 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www-aplas.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}