{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T21:55:19Z","timestamp":1743112519008,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642142024"},{"type":"electronic","value":"9783642142031"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14203-1_33","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T13:10:58Z","timestamp":1278940258000},"page":"384-399","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":29,"title":["An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic"],"prefix":"10.1007","author":[{"given":"Angelo","family":"Brillout","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Wahl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,7,13]]},"reference":[{"key":"33_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-540-70545-1_29","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2008","unstructured":"Beyer, D., Zufferey, D., Majumdar, R.: CSIsat: Interpolation for LA+EUF. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 304\u2013308. Springer, Heidelberg (2008)"},{"key":"33_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-642-02959-2_15","volume-title":"CADE 2009","author":"A. Cimatti","year":"2009","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Interpolant generation for UTVPI. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol.\u00a05663, pp. 167\u2013182. Springer, Heidelberg (2009)"},{"issue":"3","key":"33_CR3","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. The Journal of Symbolic Logic\u00a022(3), 250\u2013268 (1957)","journal-title":"The Journal of Symbolic Logic"},{"key":"33_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M.C. Fitting","year":"1996","unstructured":"Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Heidelberg (1996)","edition":"2"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-540-70545-1_24","volume-title":"Computer Aided Verification","author":"H. Jain","year":"2008","unstructured":"Jain, H., Clarke, E., Grumberg, O.: Efficient interpolation for linear diophantine (dis)equations and linear modular equations. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 254\u2013267. Springer, Heidelberg (2008)"},{"issue":"4","key":"33_CR6","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1137\/0208040","volume":"8","author":"R. Kannan","year":"1979","unstructured":"Kannan, R., Bachem, A.: Polynomial algorithms for computing the Smith and Hermite normal forms of an integer matrix. SIAM J. Comput.\u00a08(4), 499\u2013507 (1979)","journal-title":"SIAM J. Comput."},{"key":"33_CR7","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1145\/1181775.1181789","volume-title":"SIGSOFT \u201906\/FSE-14","author":"D. Kapur","year":"2006","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: SIGSOFT \u201906\/FSE-14, pp. 105\u2013116. ACM, New York (2006)"},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-540-88387-6_13","volume-title":"Automated Technology for Verification and Analysis","author":"C. Lynch","year":"2008","unstructured":"Lynch, C., Tang, Y.: Interpolants for linear arithmetic in SMT. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 156\u2013170. Springer, Heidelberg (2008)"},{"key":"33_CR9","first-page":"235","volume":"12","author":"S. Maehara","year":"1960","unstructured":"Maehara, S.: On the interpolation theorem of Craig. Sugaku\u00a012, 235\u2013237 (1960)","journal-title":"Sugaku"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci.\u00a0345(1) (2005)","DOI":"10.1016\/j.tcs.2005.07.003"},{"key":"33_CR11","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":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"33_CR12","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du Ier congr\u00e8s de Math\u00e9maticiens des Pays Slaves (1929)"},{"key":"33_CR13","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"8","author":"W. Pugh","year":"1992","unstructured":"Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM\u00a08, 102\u2013114 (1992)","journal-title":"Communications of the ACM"},{"key":"33_CR14","unstructured":"R\u00fcmmer, P.: A sequent calculus for integer arithmetic with counterexample generation. In: VERIFY. CEUR, vol.\u00a0259 (2007), \nhttp:\/\/ceur-ws.org\/"},{"key":"33_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 274\u2013289. Springer, Heidelberg (2008)"},{"key":"33_CR16","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.\u00a04349, pp. 346\u2013362. Springer, Heidelberg (2007)"},{"key":"33_CR17","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1986)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14203-1_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,20]],"date-time":"2021-08-20T02:03:19Z","timestamp":1629424999000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-14203-1_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142024","9783642142031"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14203-1_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]},"assertion":[{"value":"13 July 2010","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}