{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:16:01Z","timestamp":1725484561995},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439158"},{"type":"electronic","value":"9783540456070"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45607-4_7","type":"book-chapter","created":{"date-parts":[[2007,5,22]],"date-time":"2007-05-22T19:08:20Z","timestamp":1179860900000},"page":"111-128","source":"Crossref","is-referenced-by-count":9,"title":["Verification of Sets of Infinite State Processes Using Program Transformation"],"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":[]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"7_CR1","unstructured":"G. R. Andrews. Concurrent programming: principles and practice. Addison-Wesley, 1991."},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1016\/0743-1066(94)90024-8","volume":"19 20","author":"K. R. Apt","year":"1994","unstructured":"K. R. Apt and R. N. Bol. Logic programming and negation: A survey. Journal of Logic Programming, 19, 20:9\u201371, 1994.","journal-title":"Journal of Logic Programming"},{"issue":"6","key":"7_CR3","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K. R. Apt","year":"1986","unstructured":"K. R. Apt and D. C. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22(6):307\u2013309, 1986.","journal-title":"Information Processing Letters"},{"key":"7_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-46002-0_16","volume-title":"Proceedings of the Eighth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201902)\u201d","author":"M. Bozzano","year":"2002","unstructured":"M. Bozzano and G. Delzanno. Beyond parameterized verification. In Proceedings of the Eighth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201902)\u201d, Lecture Notes in Computer Science 2280, pages 221\u2013235. Springer, 2002."},{"issue":"1","key":"7_CR5","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"R. M. Burstall","year":"1977","unstructured":"R. M. Burstall and J. Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44\u201367, January 1977.","journal-title":"Journal of the ACM"},{"key":"7_CR6","unstructured":"E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000."},{"key":"7_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999)","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno and A. Podelski. Model checking in CLP. In R. Cleaveland, editor, 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999), Lecture Notes in Computer Science 1579, pages 223\u2013239. Springer-Verlag, 1999."},{"key":"7_CR8","unstructured":"H. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972."},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0304-3975(95)00148-4","volume":"166","author":"S. Etalle","year":"1996","unstructured":"S. Etalle and M. Gabbrielli. Transformations of CLP modules. Theoretical Computer Science, 166:101\u2013146, 1996.","journal-title":"Theoretical Computer Science"},{"key":"7_CR10","unstructured":"F. Fioravanti. MAP: A system for transforming constraint logic programs. available at http:\/\/www.iasi.rm.cnr.it\/~fioravan , 2001."},{"key":"7_CR11","series-title":"PhD thesis","volume-title":"Transformation of Constraint Logic Programs for Software Specialization and Verification","author":"F. Fioravanti","year":"2002","unstructured":"F. Fioravanti. Transformation of Constraint Logic Programs for Software Specialization and Verification. PhD thesis, Universit\u00e0 di Roma \u201cLa Sapienza\u201d, Italy, 2002."},{"key":"7_CR12","first-page":"85","volume-title":"Technical Report DSSE-TR-2001-3","author":"F. Fioravanti","year":"2001","unstructured":"F. Fioravanti, A. Pettorossi, and M. Proietti. Verifying CTL properties of infinite state systems by specializing constraint logic programs. In Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL\u201901, Florence (Italy), Technical Report DSSE-TR-2001-3, pages 85\u201396. University of Southampton, UK, 2001."},{"issue":"3\/4","key":"7_CR13","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1023\/A:1009747629591","volume":"2","author":"L. Fribourg","year":"1997","unstructured":"L. Fribourg and H. Ols\u00e9n. A decompositional approach for computing least fixed-points of Datalog programs with z-counters. Constraints, 2(3\/4):305\u2013335, 1997.","journal-title":"Constraints"},{"key":"7_CR14","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19\/20","author":"J. Jaffar","year":"1994","unstructured":"J. Jaffar and M. Maher. Constraint logic programming: A survey. Journal of Logic Programming, 19\/20:503\u2013581, 1994.","journal-title":"Journal of Logic Programming"},{"key":"7_CR15","unstructured":"N. Klarlund and A. M\u00f8ller. MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, Department of Computer Science, University of Aarhus, January 2001."},{"issue":"8","key":"7_CR16","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"L. Lamport. A new solution of Dijkstra\u2019s concurrent programming problem. Communications of the ACM, 17(8):453\u2013455, 1974.","journal-title":"Communications of the ACM"},{"key":"7_CR17","series-title":"Lect Notes Comput Sci","first-page":"63","volume-title":"Proceedings of LOPSTR\u2019 99, Venice, Italy","author":"M. Leuschel","year":"1999","unstructured":"M. Leuschel and T. Massart. Infinite state model checking by abstract interpretation and program specialization. In A. Bossi, editor, Proceedings of LOPSTR\u2019 99, Venice, Italy, Lecture Notes in Computer Science 1817, pages 63\u201382. Springer, 1999."},{"key":"7_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1007\/10722167_25","volume-title":"CAV 2000","author":"K. L. McMillan","year":"2000","unstructured":"K. L. McMillan, S. Qadeer, and J. B. Saxe. Induction in compositional model checking. In CAV 2000, Lecture Notes in Computer Science 1855, pages 312\u2013327. Springer, 2000."},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"U. Nilsson and J. L\u00fcbcke. Constraint logic programming for local and symbolic model-checking. In J. W. Lloyd, editor, CL 2000: Computational Logic, Lecture Notes in Artificial Intelligence 1861, pages 384\u2013398, 2000.","DOI":"10.1007\/3-540-44957-4_26"},{"key":"7_CR20","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/0743-1066(94)90028-0","volume":"1920","author":"A. Pettorossi","year":"1994","unstructured":"A. Pettorossi and M. Proietti. Transformation of logic programs: Foundations and techniques. Journal of Logic Programming, 19,20:261\u2013320, 1994.","journal-title":"Journal of Logic Programming"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"L. Prensa-Nieto. Completeness of the Owicki-Gries system for parameterized parallel programs. In Formal Methods for Parallel Programming: Theory and Applications, FMPPTA 2001. IEEE Computer Society Press, 2001.","DOI":"10.1109\/IPDPS.2001.925138"},{"key":"7_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/3-540-63166-6_16","volume-title":"CAV\u2019 97","author":"Y. S. Ramakrishna","year":"1997","unstructured":"Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In CAV\u2019 97, Lecture Notes in Computer Science 1254, pages 143\u2013154. Springer-Verlag, 1997."},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"A. Roychoudhury and I.V. Ramakrishnan. Automated inductive verification of parameterized protocols. In CAV 2001, pages 25\u201337, 2001.","DOI":"10.1007\/3-540-44585-4_4"},{"key":"7_CR24","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/0304-3975(91)90007-O","volume":"86","author":"H. Seki","year":"1991","unstructured":"H. Seki. Unfold\/fold transformation of stratified programs. Theoretical Computer Science, 86:107\u2013139, 1991.","journal-title":"Theoretical Computer Science"},{"key":"7_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44618-4_1","volume-title":"CONCUR 2000: Concurrency Theory","author":"N. Shankar","year":"2000","unstructured":"N. Shankar. Combining theorem proving and model checking through symbolic analysis. In CONCUR 2000: Concurrency Theory, number 1877 in Lecture Notes in Computer Science, pages 1\u201316, State College, PA, August 2000. Springer-Verlag."},{"key":"7_CR26","unstructured":"H. Tamaki and T. Sato. Unfold\/fold transformation of logic programs. In S.-\u00c5. T\u00e4rnlund, editor, Proceedings of the Second International Conference on Logic Programming, Uppsala, Sweden, pages 127\u2013138. Uppsala University, 1984."},{"key":"7_CR27","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BF01691346","volume":"2","author":"J. W. Thatcher","year":"1968","unstructured":"J. W. Thatcher and J. B. Wright. Generalized finite automata with an application to a decision problem of second-order logic. Mathematical System Theory, 2:57\u201382, 1968.","journal-title":"Mathematical System Theory"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume 3, pages 389\u2013455. Springer, 1997.","DOI":"10.1007\/978-3-642-59126-6_7"}],"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\/3-540-45607-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T07:00:01Z","timestamp":1556434801000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45607-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439158","9783540456070"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-45607-4_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}