{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:02:50Z","timestamp":1725487370634},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540404385"},{"type":"electronic","value":"9783540450139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45013-0_14","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:06:29Z","timestamp":1184587589000},"page":"160-181","source":"Crossref","is-referenced-by-count":1,"title":["Combining Logic Programs and Monadic Second Order Logics by 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":[[2003,6,24]]},"reference":[{"key":"14_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. Journal of Logic Programming, 19, 20:9\u201371, 1994.","journal-title":"Journal of Logic Programming"},{"key":"14_CR2","unstructured":"D. Basin and S. Friedrich. Combining WS1S and HOL. In D.M. Gabbay and M. de Rijke (eds.), Frontiers of Combining Systems 2, volume 7 of Studies in Logic and Computation, pp. 39\u201356. Research Studies Press\/Wiley, 2000."},{"issue":"3","key":"14_CR3","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1023\/A:1008644009416","volume":"13","author":"D. Basin","year":"1998","unstructured":"D. Basin and N. Klarlund. Automata based symbolic reasoning in hardware verification. The Journal of Formal Methods in Systems Design, 13(3):255\u2013288, 1998.","journal-title":"The Journal of Formal Methods in Systems Design"},{"key":"14_CR4","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"J. R. B\u00fcchi","year":"1960","unstructured":"J. R. B\u00fcchi. Weak second order arithmetic and and finite automata. Z. Maath Logik Grundlagen Math, 6:66\u201392, 1960.","journal-title":"Z. Maath Logik Grundlagen Math"},{"key":"14_CR5","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":"14_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Proc. TACAS\u201999","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno and A. Podelski. Model checking in CLP. In R. Cleaveland (ed.), Proc. TACAS\u201999, LNCS 1579, pp. 223\u2013239. Springer, 1999."},{"key":"14_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/3-540-45607-4_7","volume-title":"Proc. LOPSTR 2001","author":"F. Fioravanti","year":"2002","unstructured":"F. Fioravanti, A. Pettorossi, and M. Proietti. Verification of sets of infinite state systems using program transformation. In A. Pettorossi (ed.), Proc. LOPSTR 2001, LNCS 2372, pp. 111\u2013128. Springer, 2002."},{"key":"14_CR8","series-title":"Lect Notes Comput Sci","first-page":"96","volume-title":"Proc. CONCUR\u2019 97","author":"L. Fribourg","year":"1997","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, pp. 96\u2013107. Springer, 1997."},{"key":"14_CR9","series-title":"Lect Notes Comput Sci","first-page":"89","volume-title":"Proc. TACAS\u2019 95","author":"J. G. Henriksen","year":"1996","unstructured":"J. G. Henriksen, J. L. Jensen, M. E. J\u00f8rgensen, N. Klarlund, R. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In E. Brinksma et al. (eds.), Proc. TACAS\u2019 95, LNCS 1019, pp. 89\u2013110. Springer, 1996."},{"key":"14_CR10","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":"14_CR11","doi-asserted-by":"crossref","unstructured":"N. Klarlund, M. Nielsen, and K. Sunesen. Automated logical verification based on trace abstraction. In Proc. 15th ACM Symposium on Principles of Distributed Computing, pp. 101\u2013110. ACM, 1996.","DOI":"10.1145\/248052.248069"},{"issue":"8","key":"14_CR12","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":"14_CR13","series-title":"Lect Notes Comput Sci","first-page":"63","volume-title":"Proc. LOPSTR\u2019 99","author":"M. Leuschel","year":"1999","unstructured":"M. Leuschel and T. Massart. Infinite state model checking by abstract interpretation and program specialization. In A. Bossi (ed.), Proc. LOPSTR\u2019 99, LNCS 1817, pp. 63\u201382. Springer, 1999."},{"key":"14_CR14","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":"14_CR15","doi-asserted-by":"crossref","unstructured":"U. Nilsson and J. L\u00fcbcke. Constraint logic programming for local and symbolic model-checking. In J. W. Lloyd et al. (eds.), Proc. CL\u20192000, LNAI 1861, pp. 384\u2013398, 2000.","DOI":"10.1007\/3-540-44957-4_26"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"A. Pettorossi and M. Proietti. Perfect model checking via unfold\/fold transformations. In J. W. Lloyd et al. (eds.), Proc. CL\u20192000, LNAI 1861, pp. 613\u2013628. Springer, 2000.","DOI":"10.1007\/3-540-44957-4_41"},{"key":"14_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/3-540-45628-7_12","volume-title":"Computational Logic: Logic Programming and Beyond (in honour of Bob Kowalski, Part I)","author":"A. Pettorossi","year":"2002","unstructured":"A. Pettorossi and M. Proietti. Program Derivation = Rules + Strategies. In A. Kakas and F. Sadri (eds.), Computational Logic: Logic Programming and Beyond (in honour of Bob Kowalski, Part I), LNCS 2407, pp. 273\u2013309. Springer, 2002."},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"A. Pettorossi, M. Proietti, and S. Renault. Reducing nondeterminism while specializing logic programs. In Proc. 24-th POPL, pp. 414\u2013427. ACM Press, 1997.","DOI":"10.1145\/263699.263759"},{"key":"14_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/3-540-63166-6_16","volume-title":"Proc. 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 Proc. CAV\u2019 97, LNCS 1254, pp. 143\u2013154. Springer, 1997."},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"A. Roychoudhury and I.V. Ramakrishnan. Automated inductive verification of parameterized protocols. In Proc. CAV 2001, pp. 25\u201337, 2001.","DOI":"10.1007\/3-540-44585-4_4"},{"key":"14_CR21","unstructured":"K. Sagonas, T. Swift, D. S. Warren, J. Freire, P. Rao, B. Cui, and E. Johnson. The XSB system, version 2.2., 2000."},{"key":"14_CR22","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":"14_CR23","unstructured":"The MAP group. The MAP transformation system. Available from http:\/\/www.iasi.rm.cnr.it\/~proietti\/system.html , 1995\u20132002."},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa (eds.), Handbook of Formal Languages, volume 3, pp. 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-45013-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T23:21:51Z","timestamp":1556666511000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45013-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540404385","9783540450139"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45013-0_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}