{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T10:38:06Z","timestamp":1757587086386,"version":"3.41.2"},"reference-count":56,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,4,27]],"date-time":"2012-04-27T00:00:00Z","timestamp":1335484800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The use of interpolants in model checking is becoming an enabling technology\nto allow fast and robust verification of hardware and software. The application\nof encodings based on the theory of arrays, however, is limited by the\nimpossibility of deriving quantifier- free interpolants in general. In this\npaper, we show that it is possible to obtain quantifier-free interpolants for a\nSkolemized version of the extensional theory of arrays. We prove this in two\nways: (1) non-constructively, by using the model theoretic notion of\namalgamation, which is known to be equivalent to admit quantifier-free\ninterpolation for universal theories; and (2) constructively, by designing an\ninterpolating procedure, based on solving equations between array updates.\n(Interestingly, rewriting techniques are used in the key steps of the solver\nand its proof of correctness.) To the best of our knowledge, this is the first\nsuccessful attempt of computing quantifier- free interpolants for a variant of\nthe theory of arrays with extensionality.<\/jats:p>","DOI":"10.2168\/lmcs-8(2:4)2012","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T14:50:43Z","timestamp":1379947843000},"source":"Crossref","is-referenced-by-count":20,"title":["Quantifier-Free Interpolation of a Theory of Arrays"],"prefix":"10.46298","volume":"Volume 8, Issue 2","author":[{"given":"Roberto","family":"Bruttomesso","sequence":"first","affiliation":[]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,4,27]]},"reference":[{"key":"10.2168\/LMCS-8(2:4)2012_Bonacina","doi-asserted-by":"crossref","unstructured":"A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz. New results on rewrite-based satisfiability procedures.ACM Trans. Comput. Log., 10(1), 2009.","DOI":"10.1145\/1459010.1459014"},{"issue":"2","key":"10.2168\/LMCS-8(2:4)2012_ARR","first-page":"140","volume":"183","author":"Alessandro Armando, Silvio Ranise, and M","year":"2003","journal-title":"Inform. and Comput. RTA 2001 (Utrecht)"},{"issue":"10","key":"10.2168\/LMCS-8(2:4)2012_gaussBG","doi-asserted-by":"crossref","first-page":"1413","DOI":"10.1016\/j.ic.2005.05.009","volume":"204","author":"F. Baader, S. Ghilardi, and C. Tinelli","year":"2006","journal-title":"Inform. and Comput."},{"key":"10.2168\/LMCS-8(2:4)2012_rewriting","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow.Term rewriting and all that. Cambridge University Press, Cambridge, 1998.","DOI":"10.1017\/CBO9781139172752"},{"issue":"3","key":"10.2168\/LMCS-8(2:4)2012_superposition","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair and H. Ganzinger","year":"1994","journal-title":"J. Log. Comput."},{"key":"10.2168\/LMCS-8(2:4)2012_tiwari","doi-asserted-by":"crossref","unstructured":"L. Bachmair and A. Tiwari. Abstract Congruence Closure and Specializations. InConference on Automated Deduction, CADE '2000, volume 1831 ofLNCS, pages 64-78. Springer-Verlag, 2000.","DOI":"10.1007\/10721959_5"},{"key":"10.2168\/LMCS-8(2:4)2012_amalgam","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/BF02485230","volume":"5","author":"P. D. Bacsich","year":"1975","journal-title":"Algebra Universalis"},{"key":"10.2168\/LMCS-8(2:4)2012_BNO+08b","doi-asserted-by":"crossref","unstructured":"M. Bofill, R. Nieuwenhuis, A. Oliveras, E. Rodrguez-Carbonell, and A. Rubio. A Write-Based Solver for SAT Modulo the Theory of Arrays. InFMCAD, pages 101-108, 2008.","DOI":"10.1109\/FMCAD.2008.ECP.18"},{"key":"10.2168\/LMCS-8(2:4)2012_BBC+05c","doi-asserted-by":"crossref","unstructured":"M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. Van Rossum, S. Ranise, and R. Sebastiani. Efficient Satisfiability Modulo Theories via Delayed Theory Combination. InCAV'05, pages 335-349, 2005.","DOI":"10.1007\/11513988_34"},{"key":"10.2168\/LMCS-8(2:4)2012_bradley","unstructured":"Aaron R. Bradley and Zohar Manna.The Calculus of Computation. Springer, 2007."},{"key":"10.2168\/LMCS-8(2:4)2012_BKR+10","doi-asserted-by":"crossref","unstructured":"A. Brillout, D. Kroening, P. R\u00fcmmer, and W. Thomas. An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. InIJCAR, 2010.","DOI":"10.1007\/978-3-642-14203-1_33"},{"key":"10.2168\/LMCS-8(2:4)2012_BKR+10b","unstructured":"A. Brillout, D. Kroening, P. R\u00fcmmer, and T. Wahl. Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays. InVerification Workshop at FLoC, 2010."},{"key":"10.2168\/LMCS-8(2:4)2012_iprincess2011","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/s10817-011-9237-y","volume":"47","author":"A. Brillout, D. Kroening, P. R\u00fcmmer, and","year":"2011","journal-title":"Journal of Automated Reasoning"},{"key":"10.2168\/LMCS-8(2:4)2012_BB09b","doi-asserted-by":"crossref","unstructured":"R. Brummayer and A. Biere. Lemmas on Demand for the Extensional Theory of Arrays.JSAT, 2009.","DOI":"10.3233\/SAT190067"},{"key":"10.2168\/LMCS-8(2:4)2012_gaussRB","unstructured":"R. Bruttomesso.Problemi di combinazione nella dimostrazione automatica e nella verifica del software. Universit\u00e0 degli Studi di Milano, 2004. Master Thesis."},{"key":"10.2168\/LMCS-8(2:4)2012_frocos11","doi-asserted-by":"crossref","unstructured":"R. Bruttomesso, S. Ghilardi, and S. Ranise. A Combination of Rewriting and Constraint Solving for the Quantifier-free Interpolation of Arrays with Integer Difference Constraints. InFroCoS, 2011.","DOI":"10.1007\/978-3-642-24364-6_8"},{"key":"10.2168\/LMCS-8(2:4)2012_rta11","doi-asserted-by":"crossref","unstructured":"R. Bruttomesso, S. Ghilardi, and S. Ranise. Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. InRTA, 2011.","DOI":"10.2168\/LMCS-8(2:4)2012"},{"key":"10.2168\/LMCS-8(2:4)2012_BPS+10","doi-asserted-by":"crossref","unstructured":"R. Bruttomesso, E. Pek, N. Sharygina, and A. Tsitovich. The OpenSMT Solver. InTACAS, pages 150-153, 2010.","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"10.2168\/LMCS-8(2:4)2012_strong_amalgamability","doi-asserted-by":"crossref","unstructured":"Roberto Bruttomesso, Silvio Ghilardi, and Silvio Ranise. From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. Technical Report RI 337-12, Dipartimento di Scienze dell'Informazione, Universit\u00e0 degli Studi di Milano, 2012.","DOI":"10.1007\/978-3-642-31365-3_12"},{"key":"10.2168\/LMCS-8(2:4)2012_CK","unstructured":"C. Chang and J. H. Keisler.Model Theory. North-Holland, Amsterdam-London, third edition, 1990."},{"key":"10.2168\/LMCS-8(2:4)2012_CGS08","doi-asserted-by":"crossref","unstructured":"A. Cimatti, A. Griggio, and R. Sebastiani. Efficient Interpolant Generation in Satisfiability Modulo Theories. InTACAS, pages 397-412, 2008.","DOI":"10.1007\/978-3-540-78800-3_30"},{"key":"10.2168\/LMCS-8(2:4)2012_CGS10","first-page":"1","volume":"12","author":"A. Cimatti, A. Griggio, and R. Sebastian","year":"2010","journal-title":"ACM Trans. Comput. Logic"},{"key":"10.2168\/LMCS-8(2:4)2012_CGJ+00","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-Guided Abstraction Refinement. InCAV, pages 154-169, 2000.","DOI":"10.1007\/10722167_15"},{"key":"10.2168\/LMCS-8(2:4)2012_Cra57","doi-asserted-by":"crossref","unstructured":"W. Craig. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory.J. Symb. Log., pages 269-285, 1957.","DOI":"10.2307\/2963594"},{"key":"10.2168\/LMCS-8(2:4)2012_dMB09","doi-asserted-by":"crossref","unstructured":"L. de Moura and N. Bj\u00f8rner. Generalized, Efficient Array Decision Procedures. InFMCAD, pages 45-52, 2009.","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"10.2168\/LMCS-8(2:4)2012_interp-strength","doi-asserted-by":"crossref","unstructured":"V. D'Silva, M. Purandare, G. Weissenbacher, and D. Kroening. Interpolant Strength. InProceedings of VMCAI 2010, volume 5944 ofLNCS, pages 129-145. Springer, 2010.","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"10.2168\/LMCS-8(2:4)2012_enderton","unstructured":"H. B. Enderton.A Mathematical Introduction to Logic. Academic Press, Inc., 1972."},{"key":"10.2168\/LMCS-8(2:4)2012_KFG+09","doi-asserted-by":"crossref","unstructured":"A. Fuchs, A. Goel, J. Grundy, S. Krsti\u00c4\u0087, and C. Tinelli. Ground Interpolation for the Theory of Equality. InTACAS, pages 413-427, 2009.","DOI":"10.1007\/978-3-642-00768-2_34"},{"key":"10.2168\/LMCS-8(2:4)2012_GD07","doi-asserted-by":"crossref","unstructured":"V. Ganesh and D. L. Dill. A Decision Procedure for Bit-Vectors and Arrays. InCAV, pages 519-531, 2007.","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"10.2168\/LMCS-8(2:4)2012_AMAI","first-page":"231","volume":"50","author":"S. Ghilardi, E. Nicolini, S. Ranise, and","year":"2007","journal-title":"Annals of Mathematics and Artificial Intelligence 2007"},{"key":"10.2168\/LMCS-8(2:4)2012_GKF08","doi-asserted-by":"crossref","unstructured":"A. Goel, S. Krsti\u00c4\u0087, and A. Fuchs. Deciding Array Formulas with Frugal Axiom Instantiation. InSMT, 2008.","DOI":"10.1145\/1512464.1512468"},{"key":"10.2168\/LMCS-8(2:4)2012_Hodges","unstructured":"W. Hodges.Model Theory, volume 42 ofEncyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 1993."},{"issue":"1","key":"10.2168\/LMCS-8(2:4)2012_JCG09","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1007\/s10703-009-0069-x","volume":"35","author":"H. Jain, E. Clarke, and O. Grumberg","year":"2009","journal-title":"Form. Methods Syst. Des."},{"key":"10.2168\/LMCS-8(2:4)2012_jhala","doi-asserted-by":"crossref","unstructured":"R. Jhala and K. L. McMillan. A Practical and Complete Approach to Predicate Refinement. InTACAS, pages 459-473, 2006.","DOI":"10.1007\/11691372_33"},{"key":"10.2168\/LMCS-8(2:4)2012_jhala-array","doi-asserted-by":"crossref","unstructured":"R. Jhala and K. L. McMillan. Array Abstractions from Proofs. InCAV, pages 193-206, 2007.","DOI":"10.1007\/978-3-540-73368-3_23"},{"key":"10.2168\/LMCS-8(2:4)2012_kapur","doi-asserted-by":"crossref","unstructured":"D. Kapur. Shostak's Congruence Closure as Completion. In8th Int. Conf. on Rewriting Techniques and Applications, volume 1232 of LNCS, pages 23-37. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-62950-5_59"},{"key":"10.2168\/LMCS-8(2:4)2012_KMZ06","doi-asserted-by":"crossref","unstructured":"D. Kapur, R. Majumdar, and C. Zarba. Interpolation for Data Structures. InSIGSOFT'06\/FSE-14, pages 105-116, 2006.","DOI":"10.1145\/1181775.1181789"},{"key":"10.2168\/LMCS-8(2:4)2012_kapurzarba","unstructured":"D. Kapur and C. G. Zarba. A reduction approach to decision procedures. Technical report, Computer Science Dep., University of New Mexico, USA, 2005."},{"key":"10.2168\/LMCS-8(2:4)2012_voronkov","doi-asserted-by":"crossref","unstructured":"L. Kov\u00e1cs and A. Voronkov. Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. InFASE, pages 470-485, 2009.","DOI":"10.1007\/978-3-642-00593-0_33"},{"issue":"2","key":"10.2168\/LMCS-8(2:4)2012_Kra97","doi-asserted-by":"crossref","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J. Kraj\u00edcek","year":"1997","journal-title":"J. Symb. Log."},{"key":"10.2168\/LMCS-8(2:4)2012_levitt","unstructured":"J. Levitt.Formal Verification Thechniques for Digital Systems. PhD thesis, Department of Computer Science, Stanford University, 1996."},{"key":"10.2168\/LMCS-8(2:4)2012_lynch","unstructured":"C. Lynch and Y. Tang. Interpolants for Linear Arithmetic in SMT. InATVA, LNCS, 2010."},{"key":"10.2168\/LMCS-8(2:4)2012_mccarthy","unstructured":"J. McCarthy. Towards a Mathematical Science of Computation. InIFIP Congress, pages 21-28, 1962."},{"key":"10.2168\/LMCS-8(2:4)2012_mcmillan-z3-interpolation","unstructured":"K. McMillan. Interpolants from Z3 proofs. InProc. of FMCAD, 2011."},{"key":"10.2168\/LMCS-8(2:4)2012_McM03","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Interpolation and SAT-Based Model Checking. InCAV, pages 1-13, 2003.","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"10.2168\/LMCS-8(2:4)2012_McM04b","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. An Interpolating Theorem Prover. InTACAS, pages 16-30, 2004.","DOI":"10.1007\/978-3-540-24730-2_2"},{"issue":"1","key":"10.2168\/LMCS-8(2:4)2012_McM05","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"K. L. McMillan","year":"2005","journal-title":"Theor. Comput. Sci."},{"key":"10.2168\/LMCS-8(2:4)2012_McM04a","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Applications of Craig Interpolation to Model Checking. InTACAS, pages 1-12, 2005.","DOI":"10.1007\/978-3-540-31980-1_1"},{"key":"10.2168\/LMCS-8(2:4)2012_quantified-mcmillan","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Quantified invariant generation using an interpolating saturation prover. InTACAS, pages 413-427, 2008.","DOI":"10.1007\/978-3-540-78800-3_31"},{"issue":"3","key":"10.2168\/LMCS-8(2:4)2012_Pud97","doi-asserted-by":"crossref","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","journal-title":"J. Symb. Log."},{"key":"10.2168\/LMCS-8(2:4)2012_RRT04","doi-asserted-by":"crossref","unstructured":"S. Ranise, C. Ringeissen, and D. Tran. Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn. InICTAC, pages 372-386, 2004.","DOI":"10.1007\/978-3-540-31862-0_27"},{"key":"10.2168\/LMCS-8(2:4)2012_RS07","unstructured":"A. Rybalchenko and V. Sofronie-Stokkermans. Constraint Solving for Interpolation. InVMCAI, 2007."},{"key":"10.2168\/LMCS-8(2:4)2012_graf","doi-asserted-by":"crossref","unstructured":"H. Saidi and S. Graf. Construction of abstract state graphs with PVS. InCAV, pages 72-83, 1997.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"10.2168\/LMCS-8(2:4)2012_stokkermans","doi-asserted-by":"crossref","unstructured":"V. Sofronie-Stokkermans. Interpolation in Local Theory Extensions. InIJCAR'06: Int. Conf. on Automated Reasoning, volume 4130 ofLNCS, pages 235-250, 2006.","DOI":"10.1007\/11814771_21"},{"key":"10.2168\/LMCS-8(2:4)2012_SBD+01","doi-asserted-by":"crossref","unstructured":"A. Stump, C. Barrett, D. Dill, and J. Levitt. A Decision Procedure for an Extensional Theory of Arrays. InIEEE Symposium on Logic in Computer Science, 2001.","DOI":"10.1109\/LICS.2001.932480"},{"key":"10.2168\/LMCS-8(2:4)2012_YM05","doi-asserted-by":"crossref","unstructured":"G. Yorsh and M. Musuvathi. A Combination Method for Generating Interpolants. InCADE, pages 353-368, 2005.","DOI":"10.1007\/11532231_26"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/934\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/934\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:59:21Z","timestamp":1681243161000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/934"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4,27]]},"references-count":56,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(2:4)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1204.2386","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1204.2386","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1007\/s10703-014-0209-9","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,4,27]]},"article-number":"934"}}