{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:14:10Z","timestamp":1763468050704,"version":"3.41.2"},"reference-count":56,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2010,12,21]],"date-time":"2010-12-21T00:00:00Z","timestamp":1292889600000},"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":["216471"],"award-info":[{"award-number":["216471"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The safety of infinite state systems can be checked by a backward reachability procedure. For certain classes of systems, it is possible to prove the termination of the procedure and hence conclude the decidability of the safety problem. Although backward reachability is property-directed, it can unnecessarily explore (large) portions of the state space of a system which are not required to verify the safety property under consideration. To avoid this, invariants can be used to dramatically prune the search space. Indeed, the problem is to guess such appropriate invariants. In this paper, we present a fully declarative and symbolic approach to the mechanization of backward reachability of infinite state systems manipulating arrays by Satisfiability Modulo Theories solving. Theories are used to specify the topology and the data manipulated by the system. We identify sufficient conditions on the theories to ensure the termination of backward reachability and we show the completeness of a method for invariant synthesis (obtained as the dual of backward reachability), again, under suitable hypotheses on the theories. We also present a pragmatic approach to interleave invariant synthesis and backward reachability so that a fix-point for the set of backward reachable states is more easily obtained. Finally, we discuss heuristics that allow us to derive an implementation of the techniques in the model checker MCMT, showing remarkable speed-ups on a significant set of safety problems extracted from a variety of sources.<\/jats:p>","DOI":"10.2168\/lmcs-6(4:10)2010","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T13:29:57Z","timestamp":1316784597000},"source":"Crossref","is-referenced-by-count":65,"title":["Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis"],"prefix":"10.46298","volume":"Volume 6, Issue 4","author":[{"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7269-9285","authenticated-orcid":false,"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2010,12,21]]},"reference":[{"key":"10.2168\/LMCS-6(4:10)2010_lics","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. General decidability theorems for infinite-state systems. InProc. of LICS, pages 313-321, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"10.2168\/LMCS-6(4:10)2010_tacas06","unstructured":"P. A. Abdulla, G. Delzanno, N. B. Henda, and A. Rezine. Regular model checking without transducers. InTACAS, volume 4424 ofLNCS, pages 721-736, 2007."},{"key":"10.2168\/LMCS-6(4:10)2010_cav06","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, G. Delzanno, and A. Rezine. Parameterized verification of infinite-state processes with global conditions. InCAV, volume 4590 ofLNCS, pages 145-157, 2007.","DOI":"10.1007\/978-3-540-73368-3_17"},{"key":"10.2168\/LMCS-6(4:10)2010_vmcai08","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, and Ahmed Rezine. Handling parameterized systems with non-atomic global conditions. InProc. of VMCAI, volume 4905 ofLNCS, pages 22-36, 2008.","DOI":"10.1007\/978-3-540-78163-9_7"},{"issue":"2","key":"10.2168\/LMCS-6(4:10)2010_lossy-channels","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"Parosh Aziz Abdulla and Bengt Jonsson","year":"1996","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-6(4:10)2010_AbdullaTCS","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla and Bengt Jonsson. Model checking of systems with many identical timed processes.Theoretical Computer Science, pages 241-264, 2003.","DOI":"10.1016\/S0304-3975(01)00330-9"},{"key":"10.2168\/LMCS-6(4:10)2010_Francesco2","doi-asserted-by":"crossref","unstructured":"F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, and G. P. Rossi. Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems: a case study. InProc. of AVOCS 10, Electr. Comm. of the EASST, 2010.","DOI":"10.1007\/978-3-642-15763-9_36"},{"key":"10.2168\/LMCS-6(4:10)2010_Francesco1","doi-asserted-by":"crossref","unstructured":"F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, and G. P. Rossi. Brief Announcement: Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems--a case study. InProc. of DISC 10, number 6343 in LNCS, pages 392-394, 2010.","DOI":"10.1007\/978-3-642-15763-9_36"},{"key":"10.2168\/LMCS-6(4:10)2010_armando-boundedmc-and-smt","doi-asserted-by":"crossref","unstructured":"A. Armando, J. Mantovani, and L. Platania. Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers. InProc. of SPIN'06, number 3925 in LNCS, pages 146-162, 2006.","DOI":"10.1007\/11691617_9"},{"key":"10.2168\/LMCS-6(4:10)2010_BaaNi","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow.Term Rewriting and All That. Cambridge University Press, United Kingdom, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"10.2168\/LMCS-6(4:10)2010_BaGh","doi-asserted-by":"crossref","first-page":"535","DOI":"10.2178\/jsl\/1185803623","volume":"72","author":"Franz Baader and Silvio Ghilardi","year":"2007","journal-title":"Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-6(4:10)2010_BFPZ05","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_39"},{"key":"10.2168\/LMCS-6(4:10)2010_rybalchenko","doi-asserted-by":"crossref","unstructured":"D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko. Invariant Synthesis for Combined Theories. InVMCAI'07, volume 4349 ofLNCS, 2007.","DOI":"10.1007\/978-3-540-69738-1_27"},{"key":"10.2168\/LMCS-6(4:10)2010_bjorner-browne-manna-cp95","doi-asserted-by":"crossref","unstructured":"N. Bj\u00f8rner, A. Browne, and Z. Manna. Automatic Generation of Invariants and Assertions. InPrinciples and Practice of Constraint Programming - CP'95, First International Conference, CP'95, Cassis, France, volume 976 ofLNCS, pages 589-623. Springer, 1995.","DOI":"10.1007\/3-540-60299-2_37"},{"key":"10.2168\/LMCS-6(4:10)2010_bouajjani-rew","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, P. Habermehl, Y. Yurski, and M. Sighireanu. Rewriting systems with data. InProc. of Symp. on Fund. of Comp. Th. (FCT 07), pages 1-22, 2007.","DOI":"10.1007\/978-3-540-74240-1_1"},{"key":"10.2168\/LMCS-6(4:10)2010_bradleymanna","unstructured":"Aaron R. Bradley and Zohar Manna. Property-Directed Incremental Invariant Generation.Formal Aspects of Computing, 2009. To appear."},{"key":"10.2168\/LMCS-6(4:10)2010_arrays","doi-asserted-by":"crossref","unstructured":"Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. What's decidable about arrays? InProc. of VMCAI, volume 3855 ofLNCS, pages 427-442, 2006.","DOI":"10.1007\/11609773_28"},{"issue":"1","key":"10.2168\/LMCS-6(4:10)2010_composite-mc","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/332740.332746","volume":"9","author":"T. Bultan, R. Gerber, and C. League","year":"2000","journal-title":"ACM Trans. on Soft. Eng. an Meth."},{"issue":"4","key":"10.2168\/LMCS-6(4:10)2010_bultan-gerber-pugh","doi-asserted-by":"crossref","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan, R. Gerber, and W. Pugh","year":"1999","journal-title":"ACM Trans. on Progr. Lang. and Sys."},{"key":"10.2168\/LMCS-6(4:10)2010_verify","unstructured":"A. Carioni, S. Ghilardi, and S. Ranise. MCMT in the Land of Parametrized Timed Automata. InProc. of VERIFY 10, 2010."},{"key":"10.2168\/LMCS-6(4:10)2010_CZ","doi-asserted-by":"crossref","unstructured":"A. Chagrov and M. Zakharyaschev.Modal Logic. Clarendon Press, 1997.","DOI":"10.1093\/oso\/9780198537793.001.0001"},{"key":"10.2168\/LMCS-6(4:10)2010_CK","unstructured":"Chen-Chung Chang and Jerome H. Keisler.Model Theory. North-Holland, Amsterdam-London, third edition, 1990."},{"key":"10.2168\/LMCS-6(4:10)2010_demoura-bijoerner","doi-asserted-by":"crossref","unstructured":"L. de Moura and N. Bj\u00f8rner. Efficient e-matching for smt solvers. InProc. of CADE, LNCS, 2007.","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"10.2168\/LMCS-6(4:10)2010_demoura-bounded","doi-asserted-by":"crossref","unstructured":"L. de Moura, H. Rue\\ss, and M. Sorea. Lazy theorem proving for bounded model checking over infinite domains. InProc. CADE, volume 2392 ofLNCS, 2002.","DOI":"10.1007\/3-540-45620-1_35"},{"key":"10.2168\/LMCS-6(4:10)2010_miopapersttt","doi-asserted-by":"crossref","unstructured":"D. D\u00e9harbe and S. Ranise. Satisfiability solving for software verification.Int. Journal on STTT, volume 11, number 3, 2009.","DOI":"10.1007\/s10009-009-0105-6"},{"key":"10.2168\/LMCS-6(4:10)2010_cav-delzanno","doi-asserted-by":"crossref","unstructured":"G. Delzanno. Automatic verification of parameterized cache coherence protocols. InProc. of CAV, number 1855 in LNCS, 2000.","DOI":"10.1007\/10722167_8"},{"key":"10.2168\/LMCS-6(4:10)2010_bro2","doi-asserted-by":"crossref","unstructured":"G. Delzanno, J. Esparza, and A. Podelski. Constraint-based analysis of broadcast protocols. InProc. of CSL, volume 1683 ofLNCS, pages 50-66, 1999.","DOI":"10.1007\/3-540-48168-0_5"},{"key":"10.2168\/LMCS-6(4:10)2010_babylon","doi-asserted-by":"crossref","unstructured":"G. Delzanno, J.-F. Raskin, and L. Van Begin. Towards the automated verification of multi-threaded java programs. In8th Int. Conf. on TACAS, number 2280 in LNCS, 2002.","DOI":"10.1007\/3-540-46002-0_13"},{"key":"10.2168\/LMCS-6(4:10)2010_wlp","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E. W. Dijkstra","year":"1975","journal-title":"Communications of the ACM"},{"key":"10.2168\/LMCS-6(4:10)2010_dill-cav95","doi-asserted-by":"crossref","unstructured":"D. L. Dill and H. Wong-Toi. Verification of Real-Time Systems by Successive Over and Under Approximation. InComputer Aided Verification, 7th International Conference, Li\u00e8ge, Belgium, volume 939 ofLNCS, pages 409-422. Springer, 1995.","DOI":"10.1007\/3-540-60045-0_66"},{"key":"10.2168\/LMCS-6(4:10)2010_Dutertre06theyices","unstructured":"Bruno Dutertre and Leonardo De Moura. The yices smt solver. Technical report, Computer Science Laboratory, SRI International, 2006. Available at http:\/\/yices.csl.sri.com."},{"key":"10.2168\/LMCS-6(4:10)2010_enderton","unstructured":"Herbert B. Enderton.A Mathematical Introduction to Logic. Academic Press, New York-London, 1972."},{"key":"10.2168\/LMCS-6(4:10)2010_bro1","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. InProc. of LICS, pages 352-359. IEEE Computer Society, 1999.","DOI":"10.1109\/LICS.1999.782630"},{"key":"10.2168\/LMCS-6(4:10)2010_qaaderflanagan","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"10.2168\/LMCS-6(4:10)2010_gallier","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0168-0072(91)90022-E","volume":"53","author":"J. Gallier","year":"1991","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.2168\/LMCS-6(4:10)2010_barret-tinelli","unstructured":"Y. Ge, C. Barrett, and C. Tinelli. Solving quantified verification conditions using satisfiability modulo theories. InProc. of CADE-21, LNCS, 2007."},{"key":"10.2168\/LMCS-6(4:10)2010_ijcar08","unstructured":"S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli. Towards SMT Model-Checking of Array-based Systems. InProc. of IJCAR, LNCS, 2008. Extended version available online as Tech. Report RI318-08 at http:\/\/homes.dsi.unimi.it\/ zucchell\/publications\/techreport\/GhiNiRaZu-RI318-08.pdf."},{"key":"10.2168\/LMCS-6(4:10)2010_stop","unstructured":"S. Ghilardi and S. Ranise. A Note on the Stopping Failures Models. 2009. Unpublished Draft, available from cmt web site."},{"key":"10.2168\/LMCS-6(4:10)2010_tableaux09","doi-asserted-by":"crossref","unstructured":"S. Ghilardi and S. Ranise. Goal Directed Invariant Synthesis for Model Checking Modulo Theories. In(TABLEAUX 09), LNAI, pages 173-188. Springer, 2009.","DOI":"10.1007\/978-3-642-02716-1_14"},{"key":"10.2168\/LMCS-6(4:10)2010_afm09","unstructured":"S. Ghilardi and S. Ranise. Model Checking Modulo Theory at work: the integration of Yices in MCMT. InAFM 09 (co-located with CAV09), 2009."},{"key":"10.2168\/LMCS-6(4:10)2010_ijcar10","doi-asserted-by":"crossref","unstructured":"S. Ghilardi and S. Ranise. MCMT: a Model Checker Modulo Theories. InProc. of IJCAR'10, LNCS, 2010. To appear.","DOI":"10.1007\/978-3-642-14203-1_3"},{"key":"10.2168\/LMCS-6(4:10)2010_avocs08","unstructured":"S. Ghilardi, S. Ranise, and T. Valsecchi. Light-Weight SMT-based Model-Checking. InProc. of AVOCS 07-08, ENTCS, 2008."},{"key":"10.2168\/LMCS-6(4:10)2010_popl05","doi-asserted-by":"crossref","unstructured":"D. Gopan, T. Reps, and M. Sagiv. Numeric analysis of array operations. InConference Record of the Thirty-Second ACM Symposium on Principles of Programming Languages, (Long Beach, CA), 338-350, 2005.","DOI":"10.1145\/1047659.1040333"},{"key":"10.2168\/LMCS-6(4:10)2010_seminal","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Sa\u00efdi. Construction of abstract state graphs with PVS. InProc. of CAV 1997, volume 1254 ofLNCS. Springer, 1997.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"10.2168\/LMCS-6(4:10)2010_henzinger-hytech","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HYTECH: A Model Checker for Hybrid Systems. InComputer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, volume 1254 ofLNCS, pages 460-463. Springer, 1997.","DOI":"10.1007\/3-540-63166-6_48"},{"key":"10.2168\/LMCS-6(4:10)2010_indexedabs","doi-asserted-by":"publisher","DOI":"10.1145\/1297658.1297662"},{"key":"10.2168\/LMCS-6(4:10)2010_dalg","unstructured":"Nancy A. Lynch.Distributed Algorithms. Morgan Kaufmann, 1996."},{"key":"10.2168\/LMCS-6(4:10)2010_approx","doi-asserted-by":"crossref","unstructured":"A. Rezine P. A. Abdulla, G. Delzanno. Approximated context-sensitive analysis for parametrized verification. InProc. of FORTE 09, LNCS, 2009.","DOI":"10.1007\/978-3-642-02138-1_3"},{"key":"10.2168\/LMCS-6(4:10)2010_park-dill-pvs","doi-asserted-by":"publisher","DOI":"10.1145\/237502.237573"},{"issue":"5","key":"10.2168\/LMCS-6(4:10)2010_lossy2","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/S0020-0190(01)00337-4","volume":"83","author":"Schnoebelen Philippe","year":"2002","journal-title":"Information Processing Letters"},{"key":"10.2168\/LMCS-6(4:10)2010_pnueli","doi-asserted-by":"crossref","unstructured":"A. Pnueli, S. Ruath, and L. D. Zuck. Automatic deductive verification with invisible invariants. InProc. of TACAS 2001, volume 2031 ofLNCS, 2001.","DOI":"10.1007\/3-540-45319-9_7"},{"key":"10.2168\/LMCS-6(4:10)2010_smt-lib","unstructured":"S. Ranise and C. Tinelli. The SMT-LIB Standard: Version 1.2. Technical report, Dep. of Comp. Science, Iowa, 2006. Available at http:\/\/www.SMT-LIB.org\/papers."},{"key":"10.2168\/LMCS-6(4:10)2010_smtlib","unstructured":"Silvio Ranise and Cesare Tinelli. The SMT-LIB standard: Version 1.2. Technical report, 2006. Available at http:\/\/combination.cs.uiowa.edu\/smtlib\/papers\/format-v1.2-r06.08.30.pdf ."},{"key":"10.2168\/LMCS-6(4:10)2010_L1","doi-asserted-by":"crossref","unstructured":"A. W. Roscoe, R. S. Lazic, and T. C. Newcomb. On model checking data-independent systems with arrays without reset.Theory and Practice of Logic Programming, pages 659-693, 2004.","DOI":"10.1017\/S1471068404002054"},{"key":"10.2168\/LMCS-6(4:10)2010_L2","unstructured":"A. W. Roscoe, R. S. Lazic, and Tom Newcomb. On model checking data-independent systems with arrays with whole-array operations. InCommunicating Sequential Processes. SpringerLNCS, 2005."},{"key":"10.2168\/LMCS-6(4:10)2010_voronkov-cav02","doi-asserted-by":"crossref","unstructured":"T. Rybina and A. Voronkov. Using canonical representations of solutions to speed up infinite-state model checking. InProc. of CAV, number 2404 in LNCS, 2002.","DOI":"10.1007\/3-540-45657-0_32"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/966\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/966\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T21:28:34Z","timestamp":1741728514000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/966"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12,21]]},"references-count":56,"URL":"https:\/\/doi.org\/10.2168\/lmcs-6(4:10)2010","relation":{"references":[{"id-type":"doi","id":"10.1007\/11609773_28","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1010.1872","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1010.1872","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2010,12,21]]},"article-number":"966"}}