{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:58:22Z","timestamp":1725469102741},"publisher-location":"Berlin\/Heidelberg","reference-count":21,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540232451"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/3-540-32370-8_7","type":"book-chapter","created":{"date-parts":[[2006,8,12]],"date-time":"2006-08-12T16:23:20Z","timestamp":1155399800000},"page":"99-116","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Proofs of Protocols via 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","reference":[{"issue":"20","key":"7_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1016\/0743-1066(94)90024-8","volume":"19","author":"K. R. Apt","year":"1994","unstructured":"K. R. Apt and R.N. Bol. Logic programming and negation: A survey. J. Logic Programming, 19,20:9\u201371, 1994.","journal-title":"J. Logic Programming"},{"issue":"1","key":"7_CR2","doi-asserted-by":"publisher","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 pro-grams. JACM, 24(1):44\u201367, January 1977.","journal-title":"JACM"},{"issue":"l","key":"7_CR3","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0304-3975(99)00231-5","volume":"240","author":"L. Cardelli","year":"2000","unstructured":"L. Cardelli and A.D. Gordon. Mobile ambients. Theoretical Computer Science, 240(l):177\u2013213,2000.","journal-title":"Theoretical Computer Science"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"W. Chen and D.S. Warren. Tabled evaluation with delaying for general logic programs. JACM, 43(1), 1996.","DOI":"10.1145\/227595.227597"},{"key":"7_CR5","unstructured":"E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"G. Delzanno. Automatic verification of parametrized cache coherence protocol. In Proc. CAV 2000, LNCS 1855, 55\u201368. Springer, 2000.","DOI":"10.1007\/10722167_8"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"G. Delzanno and A. Podelski. Model checking in CLP. In R. Cleaveland (ed.) Proc. TACAS \u203299, LNCS 1579, 223\u2013239. Springer, 1999.","DOI":"10.1007\/3-540-49059-0_16"},{"key":"7_CR8","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_CR9","doi-asserted-by":"crossref","unstructured":"F. Fioravanti, A. Pettorossi, and M. Proietti. Verifying CTL properties of infinite state systems by specializing constraint logic programs. R. 544, IASI-CNR, Roma, Italy, 2001.","DOI":"10.1007\/3-540-45142-0_8"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"L. Fribourg and H. Ols\u00e9n. Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In Proc. CONCUR\u2019 97, LNCS 1243, 96\u2013107. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63141-0_15"},{"issue":"8","key":"7_CR11","doi-asserted-by":"crossref","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. CACM, 17(8):453\u2013455, 1974.","journal-title":"CACM"},{"key":"7_CR12","unstructured":"M. Leuschel and T. Massart. Infinite state model checking by abstract interpretation and program specialization. In Proc. LOPSTR\u2019 99, LNCS 1817, 63\u201382. Springer, 1999."},{"key":"7_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-83189-8","volume-title":"Foundations of Logic Programming","author":"J.W. Lloyd","year":"1987","unstructured":"J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987."},{"key":"7_CR14","unstructured":"MAP group. The MAP transformation system. Available from: http:\/\/www.iasi.rm.cnr.it\/~proietti\/system.html,1995\u20132004."},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"K. Marriott and P. Stuckey. Programming with Constraints: An Introduction. The MIT Press, 1998.","DOI":"10.7551\/mitpress\/5625.001.0001"},{"issue":"1","key":"7_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes. Part I and II. Information and Computation, 100(1): 1\u201377, 1992.","journal-title":"Information and Computation"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"U. Nilsson and J. L\u00fcbcke. Constraint logic programming for local and symbolic model-checking. In Proc. CL 2000, LNAI 1861, 384\u2013398. Springer, 2000.","DOI":"10.1007\/3-540-44957-4_26"},{"key":"7_CR18","doi-asserted-by":"crossref","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 Proc. CAV\u2019 97, LNCS 1254, 143\u2013154. Springer, 1997.","DOI":"10.1007\/3-540-63166-6_16"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"A. Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan, I.V. Ramakrishnan, and S.A. Smolka. Verification of parameterized systems using logic program transformations. In Proc. TACAS 2000, LNCS 1785, 172\u2013187. Springer, 2000.","DOI":"10.1007\/3-540-46419-0_13"},{"key":"7_CR20","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_CR21","unstructured":"H. Tamaki and T. Sato. Unfold\/fold transformation of logic programs. In S.-\u00c5. T\u00e4rnlund (ed.) Proc. 2nd Int. Conf. Logic Programming, 127\u2013138, Uppsala, Sweden, 1984."}],"container-title":["Advances in Soft Computing","Monitoring, Security, and Rescue Techniques in Multiagent Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-32370-8_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:53:15Z","timestamp":1605646395000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-32370-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540232451"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-32370-8_7","relation":{},"subject":[]}}