{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T03:07:33Z","timestamp":1725937653261},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496732"},{"type":"electronic","value":"9783662496749"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","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":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_41","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"625-641","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Interpolants in Nonlinear Theories Over the Reals"],"prefix":"10.1007","author":[{"given":"Sicun","family":"Gao","sequence":"first","affiliation":[]},{"given":"Damien","family":"Zufferey","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"41_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/978-3-662-46669-8_26","volume-title":"Programming Languages and Systems","author":"A Albargouthi","year":"2015","unstructured":"Albargouthi, A., Berdine, J., Cook, B., Kincaid, Z.: Spatial interpolants. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 634\u2013660. Springer, Heidelberg (2015)"},{"key":"41_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-27940-9_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: Whale: an interpolation-based algorithm for inter-procedural verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 39\u201355. Springer, Heidelberg (2012)"},{"key":"41_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1007\/978-3-642-31424-7_48","volume-title":"Computer Aided Verification","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: a framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 672\u2013678. Springer, Heidelberg (2012)"},{"issue":"4","key":"41_CR4","doi-asserted-by":"publisher","first-page":"903","DOI":"10.1109\/TRO.2014.2312453","volume":"30","author":"M Althoff","year":"2014","unstructured":"Althoff, M., Dolan, J.M.: Online verification of automated road vehicles using reachability analysis. IEEE Trans. Robot. 30(4), 903\u2013918 (2014)","journal-title":"IEEE Trans. Robot."},{"key":"41_CR5","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/j.scico.2014.09.011","volume":"103","author":"K Bae","year":"2015","unstructured":"Bae, K., Krisiloff, J., Meseguer, J., \u00d6lveczky, P.C.: Designing and verifying distributed cyber-physical systems usingmultirate pals: an airplane turning control system case study. sci. comput. program. 103, 13\u201350 (2015). Selected papers from the First International Workshop on FormalTechniques for Safety-Critical Systems (FTSCS 2012)","journal-title":"sci. comput. program."},{"key":"41_CR6","volume-title":"Handbook of Constraint Programming","author":"F Benhamou","year":"2006","unstructured":"Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming. Elsevier, Amsterdam (2006). chapter 16"},{"key":"41_CR7","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/978-0-387-68546-5_18","volume-title":"New Computational Paradigms","author":"Vasco Brattka","year":"2008","unstructured":"Brattka, V., Hertling, P., Weihrauch, K.: A tutorial on computable analysis. In: Cooper, S.B., L\u00f6we, B., Sorbi, A. (eds.) New Computational Paradigms, pp. 425\u2013491. Springer, New York (2008)"},{"key":"41_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-642-14203-1_33","volume-title":"Automated Reasoning","author":"A Brillout","year":"2010","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free presburger arithmetic. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 384\u2013399. Springer, Heidelberg (2010)"},{"key":"41_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: An analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013)"},{"key":"41_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-642-35873-9_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Christ","year":"2013","unstructured":"Christ, J., Ermis, E., Sch\u00e4f, M., Wies, T.: Flow-sensitive fault localization. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 189\u2013208. Springer, Heidelberg (2013)"},{"key":"41_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-31759-0_19","volume-title":"Model Checking Software","author":"J Christ","year":"2012","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248\u2013254. Springer, Heidelberg (2012)"},{"key":"41_CR12","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. 7795, pp. 93\u2013107. Springer, Heidelberg (2013)"},{"key":"41_CR13","doi-asserted-by":"crossref","unstructured":"Collins, G., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. In: Caviness, B., Johnson, J. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and Monographs in Symbolic Computation, pp. 174\u2013200. Springer Vienna (1998)","DOI":"10.1007\/978-3-7091-9459-1_9"},{"key":"41_CR14","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the herbrand-gentzen theorem. J. Symb. Logic 22, 250\u2013268 (1957)","journal-title":"J. Symb. Logic"},{"key":"41_CR15","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)"},{"key":"41_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-11319-2_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V D\u2019Silva","year":"2010","unstructured":"D\u2019Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 129\u2013145. Springer, Heidelberg (2010)"},{"key":"41_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-32759-9_17","volume-title":"FM 2012: Formal Methods","author":"E Ermis","year":"2012","unstructured":"Ermis, E., Sch\u00e4f, M., Wies, T.: Error invariants. In: M\u00e9ry, D., Giannakopoulou, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 187\u2013201. Springer, Heidelberg (2012)"},{"key":"41_CR18","doi-asserted-by":"crossref","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: Delta-complete decision procedures for satisfiability over the reals. In: Gramlich et al. [23], pp. 286\u2013300","DOI":"10.1007\/978-3-642-31365-3_23"},{"key":"41_CR19","doi-asserted-by":"crossref","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: Delta-decidability over the reals. IEEE Computer Society, In: LICS (2012)","DOI":"10.1109\/LICS.2012.41"},{"key":"41_CR20","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. 7898, pp. 208\u2013214. Springer, Heidelberg (2013)"},{"key":"41_CR21","unstructured":"Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo odes. In: FMCAD, IEEE (2013)"},{"key":"41_CR22","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Clarke, E.M.: Proof generation from delta-decisions. In: Winkler, F., Negru, V., Ida, T., Jebelean, T., Petcu, D., Watt, S.M., Zaharie, D. (eds.) SYNASC. IEEE (2014)","DOI":"10.1109\/SYNASC.2014.29"},{"key":"41_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-31365-3_14","volume-title":"Automated Reasoning","author":"F Boer de","year":"2012","unstructured":"de Boer, F., Bonsangue, M., Rot, J.: Automated verification of recursive programs with pointers. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 149\u2013163. Springer, Heidelberg (2012)"},{"key":"41_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-642-19835-9_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Griggio","year":"2011","unstructured":"Griggio, A., Le, T.T.H., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo linear integer arithmetic. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 143\u2013157. Springer, Heidelberg (2011)"},{"key":"41_CR25","unstructured":"Hales, T., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. ArXiv e-prints, January 2015"},{"key":"41_CR26","series-title":"Lecture Notes in Computer Science","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.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012)"},{"key":"41_CR27","doi-asserted-by":"crossref","unstructured":"Kapinski, J., Deshmukh, J.V., Sankaranarayanan, S., Arechiga, N.: Simulation-guided lyapunov analysis for hybrid dynamical systems. In: Fr\u00e4nzle, M., Lygeros, J. (eds.) HSCC. ACM (2014)","DOI":"10.1145\/2562059.2562139"},{"key":"41_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-662-46681-0_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Kong","year":"2015","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \n                      \n                        \n                      \n                      $$\\delta $$\n                    -reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200\u2013205. Springer, Heidelberg (2015)"},{"key":"41_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/978-3-319-12982-2_8","volume-title":"Computational Methods in Systems Biology","author":"B Liu","year":"2014","unstructured":"Liu, B., Kong, S., Gao, S., Zuliani, P., Clarke, E.M.: Parameter synthesis for cardiac cell hybrid models using \n                      \n                        \n                      \n                      $$\\delta $$\n                    -decisions. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) CMSB 2014. LNCS, vol. 8859, pp. 99\u2013113. Springer, Heidelberg (2014)"},{"key":"41_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"41_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-24730-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2004","unstructured":"McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16\u201330. Springer, Heidelberg (2004)"},{"key":"41_CR32","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)"},{"key":"41_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-540-69738-1_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"KL McMillan","year":"2007","unstructured":"McMillan, K.L.: Interpolants and symbolic model checking. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 89\u201390. Springer, Heidelberg (2007)"},{"key":"41_CR34","unstructured":"McMillan, K.L.: Interpolants from Z3 proofs. In: Bjesse, P., Slobodov\u00e1, A. (eds.) FMCAD. FMCAD Inc. (2011)"},{"key":"41_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-23702-7_1","volume-title":"Static Analysis","author":"KL McMillan","year":"2011","unstructured":"McMillan, K.L.: Widening and interpolation. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, p. 1. Springer, Heidelberg (2011)"},{"key":"41_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-642-02658-4_35","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2009","unstructured":"McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 462\u2013476. Springer, Heidelberg (2009)"},{"issue":"3","key":"41_CR37","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic 62(3), 981\u2013998 (1997)","journal-title":"J. Symbolic Logic"},{"key":"41_CR38","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)"},{"key":"41_CR39","doi-asserted-by":"crossref","unstructured":"Sch\u00e4f, M., Schwartz-Narbonne, D., Wies, T.: Explaining inconsistent code. In: Meyer, B., Baresi, L., Mezini, M. (eds.) ACM SIGSOFT. ACM (2013)","DOI":"10.1145\/2491411.2491448"},{"key":"41_CR40","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-56999-9","volume-title":"Computable Analysis","author":"Klaus Weihrauch","year":"2000","unstructured":"Weihrauch, K., Analysis, C.: An Introduction (2000)"},{"key":"41_CR41","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/11532231_26","volume-title":"Automated Deduction \u2013 CADE-20","author":"G Yorsh","year":"2005","unstructured":"Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 353\u2013368. Springer, Heidelberg (2005)"},{"key":"41_CR42","unstructured":"Zufferey, D., Mehta, A., DelPreto, J., Sidiroglou-Douskos, S., Rinard, M., Rus, D.: Talos: Full stack robot compilation, simulation, and synthesis.Submitted to ICRA 2016 (2016)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T01:15:50Z","timestamp":1585012550000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}