{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:33:54Z","timestamp":1742913234781,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642205507"},{"type":"electronic","value":"9783642205514"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-20551-4_11","type":"book-chapter","created":{"date-parts":[[2011,4,20]],"date-time":"2011-04-20T12:04:40Z","timestamp":1303301080000},"page":"164-183","source":"Crossref","is-referenced-by-count":4,"title":["Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation"],"prefix":"10.1007","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":"297","reference":[{"key":"11_CR1","first-page":"313","volume-title":"Proc. LICS 1996","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proc. LICS 1996, pp. 313\u2013321. IEEE Press, Los Alamitos (1996)"},{"issue":"5","key":"11_CR2","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1142\/S0129054109006887","volume":"20","author":"P.A. Abdulla","year":"2009","unstructured":"Abdulla, P.A., Delzanno, G., Ben Henda, N., Rezine, A.: Monotonic abstraction (On efficient verification of parameterized systems). International Journal of Foundations of Computer Science\u00a020(5), 779\u2013801 (2009)","journal-title":"International Journal of Foundations of Computer Science"},{"issue":"20","key":"11_CR3","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1016\/0743-1066(94)90024-8","volume":"19","author":"K.R. Apt","year":"1994","unstructured":"Apt, K.R., Bol, R.N.: Logic programming and negation: A survey. Journal of Logic Programming\u00a019(20), 9\u201371 (1994)","journal-title":"Journal of Logic Programming"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-642-17511-4_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G. Banda","year":"2010","unstructured":"Banda, G., Gallagher, J.P.: Constraint-based abstract semantics for temporal logic: A direct approach to design and implementation. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 27\u201345. Springer, Heidelberg (2010)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-46419-0_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Bultan","year":"2000","unstructured":"Bultan, T.: BDD vs. Constraint-based model checking: An experimental evaluation for asynchronous concurrent systems. In: Graf, S. (ed.) TACAS 2000. LNCS, vol.\u00a01785, pp. 441\u2013455. Springer, Heidelberg (2000)"},{"issue":"4","key":"11_CR6","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM TOPLAS\u00a021(4), 747\u2013789 (1999)","journal-title":"ACM TOPLAS"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Chen, W., Warren, D.S.: Tabled evaluation with delaying for general logic programs. JACM\u00a043(1) (1996)","DOI":"10.1145\/227595.227597"},{"issue":"5","key":"11_CR8","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR9","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"11_CR10","first-page":"84","volume-title":"Proc. POPL 1978","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. POPL 1978, pp. 84\u201396. ACM Press, New York (1978)"},{"issue":"2","key":"11_CR11","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems\u00a019(2), 253\u2013291 (1997)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"11_CR12","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1023\/A:1026276129010","volume":"23","author":"G. Delzanno","year":"2003","unstructured":"Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. Formal Methods in System Design\u00a023(3), 257\u2013301 (2003)","journal-title":"Formal Methods in System Design"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-48168-0_5","volume-title":"Computer Science Logic","author":"G. Delzanno","year":"1999","unstructured":"Delzanno, G., Esparza, J., Podelski, A.: Constraint-based analysis of broadcast protocols. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 50\u201366. Springer, Heidelberg (1999)"},{"issue":"3","key":"11_CR14","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/s100090100049","volume":"3","author":"G. Delzanno","year":"2001","unstructured":"Delzanno, G., Podelski, A.: Constraint-based deductive model checking. International Journal on Software Tools for Technology Transfer\u00a03(3), 250\u2013270 (2001)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"2","key":"11_CR15","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002360050074","volume":"34","author":"J. Esparza","year":"1997","unstructured":"Esparza, J.: Decidability of model checking for infinite-state concurrent systems. Acta Informatica\u00a034(2), 85\u2013107 (1997)","journal-title":"Acta Informatica"},{"key":"11_CR16","unstructured":"Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite state systems by specializing constraint logic programs. Proc. VCL 2001, Tech.\u00a0Rep. DSSE-TR-2001-3, pp. 85\u201396. University of Southampton, UK (2001)"},{"key":"11_CR17","unstructured":"Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying infinite state systems by specializing constraint logic programs. Report\u00a0657, IASI-CNR, Roma, Italy (2007)"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","first-page":"96","volume-title":"CONCUR\u201997: Concurrency Theory","author":"L. Fribourg","year":"1997","unstructured":"Fribourg, L., Ols\u00e9n, H.: Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 96\u2013107. Springer, Heidelberg (1997)"},{"issue":"1","key":"11_CR19","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1016\/j.jcss.2005.09.001","volume":"72","author":"G. Geeraerts","year":"2006","unstructured":"Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, Enlarge and Check: New algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci.\u00a072(1), 180\u2013203 (2006)","journal-title":"J. Comput. Syst. Sci."},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"CONCUR 2001 - Concurrency Theory","author":"P. Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 426\u2013440. Springer, Heidelberg (2001)"},{"issue":"1-2","key":"11_CR21","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: A model checker for hybrid systems. International Journal on Software Tools for Technology Transfer\u00a01(1-2), 110\u2013122 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"11_CR22","unstructured":"Henriksen, K.S., Banda, G., Gallagher, J.P.: Experiments with a convex polyhedral analysis tool for logic programs. In: Proc. WLPE 2007. CoRR (2007)"},{"key":"11_CR23","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/S1571-0661(05)80429-3","volume":"9","author":"D. Lesens","year":"1997","unstructured":"Lesens, D., Sa\u00efdi, H.: Abstraction of parameterized networks. Electronic Notes of Theoretical Computer Science\u00a09, 41 (1997)","journal-title":"Electronic Notes of Theoretical Computer Science"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/3-540-48958-4_11","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M. Leuschel","year":"1999","unstructured":"Leuschel, M.: Improving homeomorphic embedding for online termination. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol.\u00a01559, pp. 199\u2013218. Springer, Heidelberg (1999)"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/3-540-36377-7_17","volume-title":"The Essence of Computation","author":"M. Leuschel","year":"2002","unstructured":"Leuschel, M.: Homeomorphic embedding for online termination of symbolic methods. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol.\u00a02566, pp. 379\u2013403. Springer, Heidelberg (2002)"},{"key":"11_CR26","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-44957-4_7","volume-title":"Computational Logic - CL 2000","author":"M. Leuschel","year":"2000","unstructured":"Leuschel, M., Lehmann, H.: Coverability of reset Petri nets and other well-structured transition systems by partial deduction. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 101\u2013115. Springer, Heidelberg (2000)"},{"issue":"1","key":"11_CR27","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1145\/271510.271525","volume":"20","author":"M. Leuschel","year":"1998","unstructured":"Leuschel, M., Martens, B., De Schreye, D.: Controlling generalization and polyvariance in partial deduction of normal logic programs. ACM Transactions on Programming Languages and Systems\u00a020(1), 208\u2013258 (1998)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/10720327_5","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M. Leuschel","year":"2000","unstructured":"Leuschel, M., Massart, T.: Infinite state model checking by abstract interpretation and program specialization. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol.\u00a01817, pp. 63\u201382. Springer, Heidelberg (2000)"},{"key":"11_CR29","unstructured":"The MAP Transformation System (2010), http:\/\/www.iasi.cnr.it\/~proietti\/system.html"},{"key":"11_CR30","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/3-540-44957-4_26","volume-title":"Computational Logic - CL 2000","author":"U. Nilsson","year":"2000","unstructured":"Nilsson, U., L\u00fcbcke, J.: Constraint logic programming for local and symbolic model-checking. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 384\u2013398. Springer, Heidelberg (2000)"},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/3-540-45013-0_8","volume-title":"Logic Based Program Synthesis and Transformation","author":"J.C. Peralta","year":"2002","unstructured":"Peralta, J.C., Gallagher, J.P.: Convex hull abstractions in specialization of CLP programs. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol.\u00a02664, pp. 90\u2013108. Springer, Heidelberg (2002)"},{"issue":"3","key":"11_CR32","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G.L. Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Information Processing Letters\u00a012(3), 115\u2013116 (1981)","journal-title":"Information Processing Letters"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-61474-5_68","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"1996","unstructured":"Pnueli, A., Shahar, E.: A platform for combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 184\u2013195. Springer, Heidelberg (1996)"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-63166-6_16","volume-title":"Computer Aided Verification","author":"Y.S. Ramakrishna","year":"1997","unstructured":"Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T., Warren, D.S.: Efficient model checking using tabled resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 143\u2013154. Springer, Heidelberg (1997)"},{"key":"11_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-46419-0_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Roychoudhury","year":"2000","unstructured":"Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Verification of parameterized systems using logic program transformations. In: Graf, S. (ed.) TACAS 2000. LNCS, vol.\u00a01785, pp. 172\u2013187. Springer, Heidelberg (2000)"},{"key":"11_CR36","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/0304-3975(91)90007-O","volume":"86","author":"H. Seki","year":"1991","unstructured":"Seki, H.: Unfold\/fold transformation of stratified programs. Theoretical Computer Science\u00a086, 107\u2013139 (1991)","journal-title":"Theoretical Computer Science"},{"key":"11_CR37","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1023\/A:1008791913551","volume":"15","author":"H.B. Sipma","year":"1999","unstructured":"Sipma, H.B., Uribe, T.E., Manna, Z.: Deductive model checking. Formal Methods in System Design\u00a015, 49\u201374 (1999)","journal-title":"Formal Methods in System Design"},{"key":"11_CR38","first-page":"465","volume-title":"Proc. ILPS 1995","author":"M.H. S\u00f8rensen","year":"1995","unstructured":"S\u00f8rensen, M.H., Gl\u00fcck, R.: An algorithm of generalization in positive supercompilation. In: Proc. ILPS 1995, pp. 465\u2013479. MIT Press, Cambridge (1995)"},{"issue":"3","key":"11_CR39","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10703-009-0081-1","volume":"35","author":"T. Yavuz-Kahveci","year":"2009","unstructured":"Yavuz-Kahveci, T., Bultan, T.: Action Language Verifier: An infinite-state model checker for reactive software specifications. Formal Methods in System Design\u00a035(3), 325\u2013367 (2009)","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-20551-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,18]],"date-time":"2020-06-18T12:13:14Z","timestamp":1592482394000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-20551-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642205507","9783642205514"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-20551-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}