{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,12,1]],"date-time":"2023-12-01T01:35:51Z","timestamp":1701394551927},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2011,9,9]],"date-time":"2011-09-09T00:00:00Z","timestamp":1315526400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2011,12]]},"DOI":"10.1007\/s10817-011-9237-y","type":"journal-article","created":{"date-parts":[[2011,9,9]],"date-time":"2011-09-09T04:42:24Z","timestamp":1315543344000},"page":"341-367","source":"Crossref","is-referenced-by-count":23,"title":["An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic"],"prefix":"10.1007","volume":"47","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":[[2011,9,9]]},"reference":[{"key":"9237_CR1","doi-asserted-by":"crossref","unstructured":"Beyer, D., Zufferey, D., Majumdar, R.: CSIsat: interpolation for LA+EUF. In: CAV. LNCS, vol. 5123, pp. 304\u2013308. Springer (2008)","DOI":"10.1007\/978-3-540-70545-1_29"},{"key":"9237_CR2","unstructured":"Brillout, A.: Approximating and interpolating theories of arithmetic for software verification. Ph.D. thesis, ETH Z\u00fcrich (2011)"},{"key":"9237_CR3","doi-asserted-by":"crossref","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free Presburger arithmetic. In: Proceedings, International Joint Conference on Automated Reasoning (IJCAR). LNCS, vol. 6173, pp. 384\u2013399. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_33"},{"key":"9237_CR4","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT solver. In: TACAS, LNCS, pp. 150\u2013153. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"9237_CR5","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Interpolant generation for UTVPI. In: Schmidt, R.A. (ed.) CADE, LNCS, vol. 5663, pp. 167\u2013182. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_15"},{"issue":"3","key":"9237_CR6","doi-asserted-by":"crossref","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\u2013Gentzen theorem. J. Symb. Log. 22(3), 250\u2013268 (1957)","journal-title":"J. Symb. Log."},{"key":"9237_CR7","unstructured":"Dutertre, B., de Moura, L.: Integrating Simplex with DPLL(T). Tech. Rep. SRI-CSL-06-01, SRI International (2006)"},{"key":"9237_CR8","doi-asserted-by":"crossref","unstructured":"Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer (1996)","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"9237_CR9","doi-asserted-by":"crossref","unstructured":"Griggio, A., Le, T.T.H., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo linear integer arithmetic. In: TACAS, LNCS, vol. 6605, pp. 143\u2013157. Springer (2011)","DOI":"10.1007\/978-3-642-19835-9_13"},{"key":"9237_CR10","doi-asserted-by":"crossref","unstructured":"Jain, H., Clarke, E., Grumberg, O.: Efficient interpolation for linear diophantine (dis)equations and linear modular equations. In: CAV, LNCS, pp. 254\u2013267. Springer (2008)","DOI":"10.1007\/978-3-540-70545-1_24"},{"issue":"4","key":"9237_CR11","doi-asserted-by":"crossref","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. 8(4), 499\u2013507 (1979)","journal-title":"SIAM J. Comput."},{"key":"9237_CR12","doi-asserted-by":"crossref","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: SIGSOFT \u201906\/FSE-14, pp. 105\u2013116. ACM (2006)","DOI":"10.1145\/1181775.1181789"},{"key":"9237_CR13","doi-asserted-by":"crossref","unstructured":"Kroening, D., Leroux, J., R\u00fcmmer, P.: Interpolating quantifier-free Presburger arithmetic. In: Proceedings, LPAR. LNCS, vol. 6397, pp. 489\u2013503. Springer (2010)","DOI":"10.1007\/978-3-642-16242-8_35"},{"key":"9237_CR14","doi-asserted-by":"crossref","unstructured":"Lynch, C., Tang, Y.: Interpolants for linear arithmetic in SMT. In: ATVA. LNCS, pp. 156\u2013170. Springer (2008)","DOI":"10.1007\/978-3-540-88387-6_13"},{"issue":"1","key":"9237_CR15","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comp. Sci. 345(1), 101\u2013121 (2005)","journal-title":"Theor. Comp. Sci."},{"key":"9237_CR16","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification (CAV). LNCS, vol. 4144, pp. 123\u2013136. Springer (2006)","DOI":"10.1007\/11817963_14"},{"key":"9237_CR17","doi-asserted-by":"crossref","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. Commun. ACM 8, 102\u2013114 (1992)","journal-title":"Commun. ACM"},{"key":"9237_CR18","unstructured":"R\u00fcmmer, P.: A sequent calculus for integer arithmetic with counterexample generation. In: Verification Workshop (VERIFY). CEUR Workshop Proceedings, vol. 259 (2007)"},{"key":"9237_CR19","unstructured":"R\u00fcmmer, P.: Calculi for program incorrectness and arithmetic. Ph.D. thesis, University of Gothenburg (2008)"},{"key":"9237_CR20","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Proceedings, LPAR. LNCS, vol. 5330, pp. 274\u2013289. Springer (2008)","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"9237_CR21","doi-asserted-by":"crossref","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Proceedings, VMCAI. LNCS, vol. 4349, pp. 346\u2013362. Springer (2007)","DOI":"10.1007\/978-3-540-69738-1_25"},{"key":"9237_CR22","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley (1986)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9237-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-011-9237-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9237-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,15]],"date-time":"2019-06-15T06:04:36Z","timestamp":1560578676000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-011-9237-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9,9]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["9237"],"URL":"https:\/\/doi.org\/10.1007\/s10817-011-9237-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,9,9]]}}}