{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:01:44Z","timestamp":1760061704565,"version":"3.41.2"},"reference-count":25,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T00:00:00Z","timestamp":1344556800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["226070"],"award-info":[{"award-number":["226070"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The problem of computing Craig interpolants in SAT and SMT has recently\nreceived a lot of interest, mainly for its applications in formal verification.\nEfficient algorithms for interpolant generation have been presented for some\ntheories of interest ---including that of equality and uninterpreted functions,\nlinear arithmetic over the rationals, and their combination--- and they are\nsuccessfully used within model checking tools. For the theory of linear\narithmetic over the integers (LA(Z)), however, the problem of finding an\ninterpolant is more challenging, and the task of developing efficient\ninterpolant generators for the full theory LA(Z) is still the objective of\nongoing research. In this paper we try to close this gap. We build on previous\nwork and present a novel interpolation algorithm for SMT(LA(Z)), which exploits\nthe full power of current state-of-the-art SMT(LA(Z)) solvers. We demonstrate\nthe potential of our approach with an extensive experimental evaluation of our\nimplementation of the proposed algorithm in the MathSAT SMT solver.<\/jats:p>","DOI":"10.2168\/lmcs-8(3:3)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T08:17:46Z","timestamp":1385713066000},"source":"Crossref","is-referenced-by-count":6,"title":["Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic"],"prefix":"10.46298","volume":"Volume 8, Issue 3","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3311-0893","authenticated-orcid":false,"given":"Alberto","family":"Griggio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thi Thieu Hoa","family":"Le","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2012,8,10]]},"reference":[{"key":"10.2168\/LMCS-8(3:3)2012_ijcar10_interpolation","doi-asserted-by":"crossref","unstructured":"Angelo Brillout, Daniel Kroening, Philipp R\u00fcmmer, and Thomas Wahl. An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. InProc. IJCAR, volume 6173 ofLNCS. Springer, 2010.","DOI":"10.1007\/978-3-642-14203-1_33"},{"key":"10.2168\/LMCS-8(3:3)2012_splitting_on_demand","doi-asserted-by":"crossref","unstructured":"C. Barrett, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. Splitting on Demand in SAT Modulo Theories. InProc. LPAR'06, volume 4246 ofLNCS. Springer, 2006.","DOI":"10.1007\/11916277_35"},{"key":"10.2168\/LMCS-8(3:3)2012_sat_handbook_lazy_smt","unstructured":"C. W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability Modulo Theories. InHandbook of Satisfiability, chapter 25. IOS Press, 2009."},{"key":"10.2168\/LMCS-8(3:3)2012_tocl_interpolation","doi-asserted-by":"crossref","unstructured":"A. Cimatti, A. Griggio, and R. Sebastiani. Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories.ACM Trans. Comput. Logic, 12(1), October 2010.","DOI":"10.1145\/1838552.1838559"},{"key":"10.2168\/LMCS-8(3:3)2012_cav09_lia","doi-asserted-by":"crossref","unstructured":"I. Dillig, T. Dillig, and A. Aiken. Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers. InProc. CAV'09, volume 5643 ofLNCS. Springer, 2009.","DOI":"10.1007\/978-3-642-02658-4_20"},{"key":"10.2168\/LMCS-8(3:3)2012_yices","doi-asserted-by":"crossref","unstructured":"B. Dutertre and L. de Moura. A Fast Linear-Arithmetic Solver for DPLL(T). InProc. CAV'06, volume 4144 ofLNCS. Springer, 2006.","DOI":"10.1007\/11817963_11"},{"key":"10.2168\/LMCS-8(3:3)2012_tinelli_tacas09","unstructured":"A. Fuchs, A. Goel, J. Grundy, S. Krstic, and C. Tinelli. Ground interpolation for the theory of equality. InProc. TACAS'09, volume 5505 ofLNCS. Springer, 2009."},{"key":"10.2168\/LMCS-8(3:3)2012_tinelli_cade09","doi-asserted-by":"crossref","unstructured":"A. Goel, S. Krstic, and C. Tinelli. Ground Interpolation for Combined Theories. InProc. CADE-22, volume 5663 ofLNCS. Springer, 2009.","DOI":"10.1007\/978-3-642-02959-2_16"},{"key":"10.2168\/LMCS-8(3:3)2012_GriggioLeSebastiani_TACAS11","doi-asserted-by":"crossref","unstructured":"A. Griggio, T.T.H. Le, and R. Sebastiani. Efficient interpolant generation in satisfiability modulo linear integer arithmetic. In Parosh Abdulla and K. Leino, editors,Tools and Algorithms for the Construction and Analysis of Systems, volume 6605 ofLecture Notes in Computer Science, pages 143-157. Springer, 2011.","DOI":"10.1007\/978-3-642-19835-9_13"},{"key":"10.2168\/LMCS-8(3:3)2012_griggio-fmcad11","unstructured":"Alberto Griggio. Effective word-level interpolation for software verification. In Per Bjesse and Anna Slobodova, editors,Proc. Formal Methods in Computer Aided Design - FMCAD11, 2011."},{"issue":"1\/2","key":"10.2168\/LMCS-8(3:3)2012_mathsat5","first-page":"1","volume":"8","author":"Alberto Griggio","year":"2012","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation - JSAT"},{"key":"10.2168\/LMCS-8(3:3)2012_AbstractionsFromProofs","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. InProc. POPL'04. ACM, 2004.","DOI":"10.1145\/964001.964021"},{"key":"10.2168\/LMCS-8(3:3)2012_jain_cav08","doi-asserted-by":"crossref","unstructured":"H. Jain, E. M. Clarke, and O. Grumberg. Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. InProc. CAV'08, volume 5123 ofLNCS. Springer, 2008.","DOI":"10.21236\/ADA476801"},{"key":"10.2168\/LMCS-8(3:3)2012_lpar10_interpolation","doi-asserted-by":"crossref","unstructured":"Daniel Kroening, J\u00e9rome Leroux, and Philipp R\u00fcmmer. Interpolating Quantifier-Free Presburger Arithmetic. InProc. LPAR, LNCS. Springer, 2010.","DOI":"10.1007\/978-3-642-16242-8_35"},{"key":"10.2168\/LMCS-8(3:3)2012_interpolation_data_structures","doi-asserted-by":"crossref","unstructured":"D. Kapur, R. Majumdar, and C. G. Zarba. Interpolation for data structures. InProc. FSE'05. ACM, 2006.","DOI":"10.1145\/1181775.1181789"},{"key":"10.2168\/LMCS-8(3:3)2012_kroening_interp","doi-asserted-by":"crossref","unstructured":"D. Kroening and G. Weissenbacher. Lifting Propositional Interpolants to the Word-Level. InProc. FMCAD'07, Los Alamitos, CA, USA, 2007. IEEE Computer Society.","DOI":"10.1109\/FAMCAD.2007.13"},{"key":"10.2168\/LMCS-8(3:3)2012_lynch_interpolation","doi-asserted-by":"crossref","unstructured":"C. Lynch and Y. Tang. Interpolants for Linear Arithmetic in SMT. InProc. ATVA'08, volume 5311 ofLNCS. Springer, 2008.","DOI":"10.1007\/978-3-540-88387-6_13"},{"key":"10.2168\/LMCS-8(3:3)2012_interpolation-mc-sat","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Interpolation and SAT-Based Model Checking. InProc. CAV'03, volume 2725 ofLNCS. Springer, 2003.","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"10.2168\/LMCS-8(3:3)2012_mcmillan_interpolating_prover","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. An interpolating theorem prover.Theor. Comput. Sci., 345(1), 2005.","DOI":"10.1016\/j.tcs.2005.07.003"},{"issue":"3","key":"10.2168\/LMCS-8(3:3)2012_pudlak_interpolation","doi-asserted-by":"crossref","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","journal-title":"J. of Symb. Logic"},{"key":"10.2168\/LMCS-8(3:3)2012_omega","doi-asserted-by":"crossref","unstructured":"W. Pugh. The Omega test: a fast and practical integer programming algorithm for dependence analysis. InProc. SC, 1991.","DOI":"10.1145\/125826.125848"},{"issue":"11","key":"10.2168\/LMCS-8(3:3)2012_rybalchenko_interp","volume":"45","author":"Andrey Rybalchenko and Viorica Sofronie-","year":"2010","journal-title":"J. Symb. Comput."},{"key":"10.2168\/LMCS-8(3:3)2012_ilp_book","unstructured":"A. Schrijver.Theory of Linear and Integer Programming. Wiley, 1986."},{"key":"10.2168\/LMCS-8(3:3)2012_tseitin","unstructured":"G. S. Tseitin. On the complexity of derivation in propositional calculus.Studies in Constructive Mathematics and Mathematical Logic, Part 2, 1968."},{"key":"10.2168\/LMCS-8(3:3)2012_musuvathi_interpolation","doi-asserted-by":"crossref","unstructured":"G. Yorsh and M. Musuvathi. A combination method for generating interpolants. InProc. CADE-20, volume 3632 ofLNCS. Springer, 2005.","DOI":"10.1007\/11532231_26"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1033\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1033\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:01:43Z","timestamp":1681243303000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1033"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,10]]},"references-count":25,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(3:3)2012","relation":{"references":[{"id-type":"doi","id":"10.2307\/2275583","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1010.4422","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1010.4422","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,8,10]]},"article-number":"1033"}}