{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,14]],"date-time":"2023-01-14T07:49:41Z","timestamp":1673682581627},"reference-count":42,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T00:00:00Z","timestamp":1327449600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2013,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic programs (CLP) and works in two phases: (1) in the first phase, a CLP specification of an infinite state system is specialized with respect to the initial state of the system and the temporal property to be verified, and (2) in the second phase, the specialized program is evaluated by using a bottom-up strategy. The effectiveness of the method strongly depends on the generalization strategy which is applied during the program specialization phase. We consider several generalization strategies obtained by combining techniques already known in the field of program analysis and program transformation, and we also introduce some new strategies. Then, through many verification experiments, we evaluate the effectiveness of the generalization strategies we have considered. Finally, we compare the implementation of our specialization-based verification method to other constraint-based model checking tools. The experimental results show that our method is competitive with the methods used by those other tools.<\/jats:p>","DOI":"10.1017\/s1471068411000627","type":"journal-article","created":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T11:32:41Z","timestamp":1327491161000},"page":"175-199","source":"Crossref","is-referenced-by-count":23,"title":["Generalization strategies for the verification of infinite state systems"],"prefix":"10.1017","volume":"13","author":[{"given":"FABIO","family":"FIORAVANTI","sequence":"first","affiliation":[]},{"given":"ALBERTO","family":"PETTOROSSI","sequence":"additional","affiliation":[]},{"given":"MAURIZIO","family":"PROIETTI","sequence":"additional","affiliation":[]},{"given":"VALERIO","family":"SENNI","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2012,1,25]]},"reference":[{"key":"S1471068411000627_ref19","first-page":"164","volume-title":"Proc. of LOPSTR 2010","author":"Fioravanti","year":"2011"},{"key":"S1471068411000627_ref40","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008791913551"},{"key":"S1471068411000627_ref39","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90007-O"},{"key":"S1471068411000627_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/325478.325480"},{"key":"S1471068411000627_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90033-7"},{"key":"S1471068411000627_ref35","first-page":"90","volume-title":"Proc. of LOPSTR 2002","author":"Peralta","year":"2003"},{"key":"S1471068411000627_ref37","first-page":"143","volume-title":"Proc. of CAV '97","author":"Ramakrishna","year":"1997"},{"key":"S1471068411000627_ref32","first-page":"63","volume-title":"Proc. of LOPSTR '99","author":"Leuschel","year":"2000"},{"key":"S1471068411000627_ref26","volume-title":"Partial Evaluation and Automatic Program Generation","author":"Jones","year":"1993"},{"key":"S1471068411000627_ref36","first-page":"184","volume-title":"Proc. of CAV '96","author":"Pnueli","year":"1996"},{"key":"S1471068411000627_ref23","first-page":"426","volume-title":"Proc. of CONCUR '01","author":"Godefroid","year":"2001"},{"key":"S1471068411000627_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0081-1"},{"key":"S1471068411000627_ref29","doi-asserted-by":"publisher","DOI":"10.1017\/S147106840200145X"},{"key":"S1471068411000627_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"key":"S1471068411000627_ref21","first-page":"96","volume-title":"Proc. of CONCUR '97","author":"Fribourg","year":"1997"},{"key":"S1471068411000627_ref12","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026276129010"},{"key":"S1471068411000627_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2005.09.001"},{"key":"S1471068411000627_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/271510.271525"},{"key":"S1471068411000627_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0064-3"},{"key":"S1471068411000627_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80429-3"},{"key":"S1471068411000627_ref18","unstructured":"Fioravanti F. , Pettorossi A. and Proietti M. 2007. Verifying infinite state systems by specializing constraint logic programs. R. 657, IASI-CNR, Roma, Italy."},{"key":"S1471068411000627_ref30","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/3-540-44957-4_7","volume-title":"Proc. of Computational Logic 2000","author":"Leuschel","year":"2000"},{"key":"S1471068411000627_ref33","unstructured":"MAP. 2011. The MAP transformation system. URL: http:\/\/www.iasi.cnr.it\/~proietti\/system.html (Version July 2011)."},{"key":"S1471068411000627_ref20","first-page":"31","volume-title":"Proc. of LOPSTR '99","author":"Fribourg","year":"2000"},{"key":"S1471068411000627_ref13","first-page":"50","volume-title":"Proc. of CSL '99","author":"Delzanno","year":"1999"},{"key":"S1471068411000627_ref28","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/3-540-36377-7_17","volume-title":"The Essence of Computation","author":"Leuschel","year":"2002"},{"key":"S1471068411000627_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90024-8"},{"key":"S1471068411000627_ref5","first-page":"441","volume-title":"Proc. of TACAS '00","author":"Bultan","year":"2000"},{"key":"S1471068411000627_ref34","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1007\/3-540-44957-4_26","volume-title":"Proc. of Computational Logic 2000","author":"Nilsson","year":"2000"},{"key":"S1471068411000627_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"S1471068411000627_ref8","volume-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"S1471068411000627_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"S1471068411000627_ref3","first-page":"27","volume-title":"Proc. of LPAR 2010","author":"Banda","year":"2010"},{"key":"S1471068411000627_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44957-4_32"},{"key":"S1471068411000627_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050074"},{"key":"S1471068411000627_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00148-4"},{"key":"S1471068411000627_ref1","doi-asserted-by":"crossref","first-page":"779","DOI":"10.1142\/S0129054109006887","article-title":"Monotonic abstraction (On efficient verification of parameterized systems)","volume":"20","author":"Abdulla","year":"2009","journal-title":"International Journal of Foundations of Computer Science"},{"key":"S1471068411000627_ref17","first-page":"85","volume-title":"Proc. of VCL'01","author":"Fioravanti","year":"2001"},{"key":"S1471068411000627_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/244795.244800"},{"key":"S1471068411000627_ref41","first-page":"465","volume-title":"Proc. of ILPS '95","author":"S\u00f8rensen","year":"1995"},{"key":"S1471068411000627_ref14","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/s100090100049","article-title":"Constraint-based deductive model checking","volume":"3","author":"Delzanno","year":"2001","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"S1471068411000627_ref38","first-page":"172","volume-title":"Proc. of TACAS 2000","author":"Roychoudhury","year":"2000"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068411000627","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,1]],"date-time":"2020-07-01T07:29:54Z","timestamp":1593588594000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068411000627\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,25]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,3]]}},"alternative-id":["S1471068411000627"],"URL":"https:\/\/doi.org\/10.1017\/s1471068411000627","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,1,25]]}}}