{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T09:05:29Z","timestamp":1725613529193},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642242878"},{"type":"electronic","value":"9783642242885"}],"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-24288-5_15","type":"book-chapter","created":{"date-parts":[[2011,9,24]],"date-time":"2011-09-24T05:46:57Z","timestamp":1316843217000},"page":"165-179","source":"Crossref","is-referenced-by-count":1,"title":["Improving Reachability Analysis of Infinite State Systems by Specialization"],"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":[{"issue":"5","key":"15_CR1","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). Int. J. of Foundations of Computer Science\u00a020(5), 779\u2013801 (2009)","journal-title":"Int. J. of Foundations of Computer Science"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/3-540-44585-4_34","volume-title":"Computer Aided Verification","author":"A. Annichini","year":"2001","unstructured":"Annichini, A., Bouajjani, A., Sighireanu, M.: TReX: A tool for reachability analysis of complex systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 368\u2013372. Springer, Heidelberg (2001)"},{"issue":"5","key":"15_CR3","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10009-008-0064-3","volume":"10","author":"S. Bardin","year":"2008","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Acceleration from theory to practice. Int. J. on Software Tools for Technology Transfer\u00a010(5), 401\u2013424 (2008)","journal-title":"Int. J. on Software Tools for Technology Transfer"},{"issue":"4","key":"15_CR4","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":"15_CR5","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":"15_CR6","first-page":"238","volume-title":"Proc. POPL 1977","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In: Proc. POPL 1977, pp. 238\u2013252. ACM Press, New York (1977)"},{"issue":"2","key":"15_CR7","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 TOPLAS\u00a019(2), 253\u2013291 (1997)","journal-title":"ACM TOPLAS"},{"issue":"3","key":"15_CR8","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"},{"issue":"3","key":"15_CR9","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. Int. J. on Software Tools for Technology Transfer\u00a03(3), 250\u2013270 (2001)","journal-title":"Int. J. on Software Tools for Technology Transfer"},{"issue":"2","key":"15_CR10","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":"15_CR11","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0304-3975(95)00148-4","volume":"166","author":"S. Etalle","year":"1996","unstructured":"Etalle, S., Gabbrielli, M.: Transformations of CLP modules. Theoretical Computer Science\u00a0166, 101\u2013146 (1996)","journal-title":"Theoretical Computer Science"},{"key":"15_CR12","unstructured":"Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite state systems by specializing constraint logic programs. In: Proc. VCL 2001, Tech. Rep. DSSE-TR-2001-3, pp. 85\u201396. Univ. of Southampton, UK (2001)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-642-20551-4_11","volume-title":"Logic-Based Program Synthesis and Transformation","author":"F. Fioravanti","year":"2011","unstructured":"Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Program specialization for verifying infinite state systems: An experimental evaluation. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol.\u00a06564, pp. 164\u2013183. Springer, Heidelberg (2011)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G. Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HYTECH. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 258\u2013273. Springer, Heidelberg (2005)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/10720327_3","volume-title":"Logic-Based Program Synthesis and Transformation","author":"L. Fribourg","year":"2000","unstructured":"Fribourg, L.: Constraint logic programming applied to model checking. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol.\u00a01817, pp. 31\u201342. Springer, Heidelberg (2000)"},{"key":"15_CR16","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)"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Proc., LICS 1996, pp. 278\u2013292 (1996)","DOI":"10.1109\/LICS.1996.561342"},{"key":"15_CR18","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19\/20","author":"J. Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.: Constraint logic programming: A survey. J. of Logic Programming\u00a019\/20, 503\u2013581 (1994)","journal-title":"J. of Logic Programming"},{"key":"15_CR19","volume-title":"Partial Evaluation and Automatic Program Generation","author":"N.D. Jones","year":"1993","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall, Englewood Cliffs (1993)"},{"key":"15_CR20","unstructured":"LASH homepage, http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash"},{"key":"15_CR21","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":"15_CR22","unstructured":"MAP homepage, http:\/\/www.iasi.cnr.it\/~proietti\/system.html"},{"key":"15_CR23","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":"2003","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 (2003)"},{"key":"15_CR24","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)"},{"issue":"3","key":"15_CR25","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","Reachability Problems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24288-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,24]],"date-time":"2020-06-24T21:54:21Z","timestamp":1593035661000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24288-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642242878","9783642242885"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24288-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}