{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:52:03Z","timestamp":1778298723840,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540672821","type":"print"},{"value":"9783540464198","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46419-0_13","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T23:17:25Z","timestamp":1186615045000},"page":"172-187","source":"Crossref","is-referenced-by-count":31,"title":["Verification of Parameterized Systems Using Logic Program Transformations"],"prefix":"10.1007","author":[{"given":"Abhik","family":"Roychoudhury","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K. Narayan","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C. R.","family":"Ramakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"I. V.","family":"Ramakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"13_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification (CAV\u2019 96)","year":"1996","unstructured":"R. Alur and T. A. Henzinger, editors. Computer Aided Verification (CAV\u2019 96), volume 1102 of Lecture Notes in Computer Science, New Brunswick, New Jersey, July 1996. Springer-Verlag. 186"},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"15","author":"K. Apt","year":"1986","unstructured":"K. Apt and D. Kozen. Limits for automatic verification of finite-state systems. Information Processing Letters, 15:307\u2013309, 1986. 178","journal-title":"Information Processing Letters"},{"issue":"1","key":"13_CR3","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M. Browne","year":"1989","unstructured":"M. Browne, E. Clarke, and O. Grumberg. Reasoning about networks with many identical finite-state processes. Information and Computation, 81(1):13\u201331, 1989. 174","journal-title":"Information and Computation"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"S. Basu, S.A. Smolka, and O.R. Ward. Model checking the Java meta-locking algorithm. In IEEE International Conference on the Engineering of Computer Based Systems. IEEE Press, April 2000. 185","DOI":"10.1109\/ECBS.2000.839894"},{"key":"13_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0016951","volume-title":"CONCUR","author":"E. Clarke","year":"1995","unstructured":"E. Clarke, O. Grumberg, and S. Jha. Verifying parametrized networks using abstraction and regular languages. In CONCUR, LNCS 962, 1995. 174"},{"key":"13_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Computer Aided Verification (CAV\u2019 96)","author":"D. L. Dill","year":"1996","unstructured":"D. L. Dill. The Mur\u03d5 verification system. In T. A. Henzinger, editors. Computer Aided Verification (CAV\u2019 96), volume 1102 of Lecture Notes in Computer Science, New Brunswick, New Jersey, July 1996 Alur and Henzinger [AH96], pages 390\u2013393. 172"},{"key":"13_CR7","series-title":"Lect Notes Comput Sci","first-page":"74","volume-title":"TACAS\u201999","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno and A. Podelski. Model checking in CLP. In TACAS\u201999, volume LNCS 1579, pages 74\u201388. Springer-Verlag, March 1999. 172"},{"key":"13_CR8","unstructured":"X. Du, C.R. Ramakrishnan, and S.A. Smolka. Tabled resolution + constraints: A recipe for model checking real-time systems. Technical report, Dept. of Computer Science, SUNY Stony Brook, http:\/\/www.cs.sunysb.edu\/~vicdu\/papers , 1999. 173"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"X. Du, S. A. Smolka, and R. Cleaveland. Local model checking and protocol analysis. Software Tools for Technology Transfer, 1999. 185","DOI":"10.1007\/s100090050031"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"E. Emerson and K.S. Namjoshi. Reasoning about rings. In POPL, pages 85\u201394, 1995. 174","DOI":"10.1145\/199448.199468"},{"key":"13_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification (CAV\u2019 96)","author":"S. Graf","year":"1996","unstructured":"S. Graf and H. Saidi. Verifying invariants using theorem proving. In T. A. Henzinger, editors. Computer Aided Verification (CAV\u2019 96), volume 1102 of Lecture Notes in Computer Science, New Brunswick, New Jersey, July 1996 Alur and Henzinger [AH96]. 174"},{"issue":"5","key":"13_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013295, May 1997. 172","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"13_CR13","first-page":"174","volume":"14","author":"C. N. Ip","year":"1999","unstructured":"C. N. Ip and D. L. Dill. Verifying systems with replicated components in Mur\u03d5. Formal Methods in System Design, 14(3), May 1999. 174","journal-title":"Formal Methods in System Design"},{"key":"13_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1995.1024","volume":"117","author":"R.P. Kurshan","year":"1995","unstructured":"R.P. Kurshan and K. Mcmillan. A structural induction theorem for processes. Information and Computation, 117:1\u201311, 1995. 174","journal-title":"Information and Computation"},{"key":"13_CR15","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"K.M.M.+.9.7._.Y. Kesten","year":"1997","unstructured":"KMM+97._Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model-checking with rich assertional languages. In CAV, LNCS 1254, 1997. 174"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parametrized linear networks of processes. In POPL, pages 346\u2013357, 1997. 174","DOI":"10.1145\/263699.263747"},{"key":"13_CR17","unstructured":"J.W. Lloyd. Foundations of Logic Programming, Second Edition. Springer-Verlag, 1993. 176"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic, 1993. 174","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"13_CR19","unstructured":"R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989. 176"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"S. Owre, N. Shankar, and J. Rushby. PVS: A Prototype Verification System. Proceedings of CADE, 1992. 174","DOI":"10.1007\/3-540-55602-8_217"},{"key":"13_CR21","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1016\/S0743-1066(99)00029-1","volume":"41","author":"A. Pettorossi","year":"1999","unstructured":"A. Pettorossi and M. Proietti. Synthesis and transformation of logic programs using unfold\/fold proofs. Journal of Logic Programming, 41, 1999. 174","journal-title":"Journal of Logic Programming"},{"key":"13_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/3-540-46674-6_27","volume-title":"ASIAN","author":"A. Roychoudhury","year":"1999","unstructured":"A. Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan, and I.V. Ramakrishnan. Beyond Tamaki-Sato style unfold\/fold transformations for normal logic programs. In ASIAN, LNCS 1742, pages 322\u2013333, 1999. 176"},{"key":"13_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/10704567_24","volume-title":"PPDP","author":"A. Roychoudhury","year":"1999","unstructured":"A. Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan, and I.V. Ramakrishnan. A parameterized unfold\/fold transformation framework for definite logic programs. In PPDP, LNCS 1702, pages 396\u2013413, 1999. 173, 178, 179"},{"key":"13_CR24","unstructured":"A. Roychoudhury. Program transformations for automated verification of parameterized concurrent systems. Technical report, Department of Computer Science, State University of New York at Stony Brook, http:\/\/www.cs.sunysb.edu\/~abhik\/papers , 1999. Dissertation proposal. 179, 182"},{"key":"13_CR25","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"R.R.R.+.9.7._.Y.S. Ramakrishna","year":"1997","unstructured":"RRR+97._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, LNCS 1254, 1997. 172, 176"},{"key":"13_CR26","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"S. Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, and M. K. Srivas. An integration of model checking with automated proof checking. In CAV, LNCS 939, 1995. 174"},{"key":"13_CR27","series-title":"Lect Notes Comput Sci","volume-title":"Constraint Programming (CP\u201996)","author":"L. Urbina","year":"1996","unstructured":"L. Urbina. Analysis of hybrid systems in CLP(R). In Constraint Programming (CP\u201996), volume LNCS 1102. Springer-Verlag, 1996. 172"},{"key":"13_CR28","series-title":"Lect Notes Comput Sci","volume-title":"Automatic Verification Methods for Finite State Systems","author":"P. Wolper","year":"1989","unstructured":"P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In Automatic Verification Methods for Finite State Systems, LNCS 407, 1989. 174"},{"key":"13_CR29","unstructured":"The XSB logic programming system v2.01, 1999. Available by anonymous ftp from http:\/\/www.cs.sunysb.edu\/~sbprolog . 185"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46419-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T21:07:09Z","timestamp":1556744829000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46419-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672821","9783540464198"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-46419-0_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}