{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:26Z","timestamp":1761611186611},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540650126"},{"type":"electronic","value":"9783540497660"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0056604","type":"book-chapter","created":{"date-parts":[[2006,7,30]],"date-time":"2006-07-30T08:19:58Z","timestamp":1154247598000},"page":"1-20","source":"Crossref","is-referenced-by-count":16,"title":["Logic programming and model checking"],"prefix":"10.1007","author":[{"given":"Baoqiu","family":"Cui","sequence":"first","affiliation":[]},{"given":"Yifei","family":"Dong","sequence":"additional","affiliation":[]},{"given":"Xiaoqun","family":"Du","sequence":"additional","affiliation":[]},{"given":"K. Narayan","family":"Kumar","sequence":"additional","affiliation":[]},{"given":"C. R.","family":"Ramakrishnan","sequence":"additional","affiliation":[]},{"given":"I. V.","family":"Ramakrishnan","sequence":"additional","affiliation":[]},{"given":"Abhik","family":"Roychoudhury","sequence":"additional","affiliation":[]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[]},{"given":"David S.","family":"Warren","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,6,2]]},"reference":[{"issue":"1","key":"1_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. Information and Computation, 104(1):2\u201334, 1993.","journal-title":"Information and Computation"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur and D. Dill. The theory of timed automata. Theoretical Computer Science, 126(2), 1994.","DOI":"10.1016\/0304-3975(94)90010-8"},{"volume-title":"volume 1102 of Lecture Notes in Computer Science","year":"1996","key":"1_CR3","unstructured":"R. Alur and T. A. Henzinger, editors. Computer Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science, New Brunswick, New Jersey, July 1996. Springer-Verlag."},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"H. R. Andersen, C. Stirling, and G. Winskel. A compositional proof system for the modal mu-calculus. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, pages 144\u2013153, Paris, France, July 1994.","DOI":"10.1109\/LICS.1994.316076"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fix-points. In ACM Symposium on Principles of Programming Languages, pages 238\u2013252. ACM Press, 1977.","DOI":"10.1145\/512950.512973"},{"key":"1_CR6","first-page":"52","volume-title":"volume 131 of Lecture Notes in Computer Science","author":"E. M. Clarke","year":"1981","unstructured":"E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In D. Kozen, editor, Proceedings of the Workshop on Logic of Programs, Yorktown Heights, volume 131 of Lecture Notes in Computer Science, pages 52\u201371. Springer-Verlag, 1981."},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2), 1986.","DOI":"10.1145\/5397.5399"},{"key":"1_CR8","first-page":"398","volume-title":"volume 1102 of Lecture Notes in Computer Science","author":"R. Cleaveland","year":"1996","unstructured":"R. Cleaveland, P. M. Lewis, S. A. Smolka, and O. Sokolsky. The Concurrency Factory: A development environment for concurrent systems. In Alur and Henzinger [AH96], pages 398\u2013401."},{"key":"1_CR9","first-page":"419","volume-title":"volume 1102 of Lecture Notes in Computer Science","author":"E. M. Clarke","year":"1996","unstructured":"E. M. Clarke, K. McMillan, S. Campos, and V. Hartonas-GarmHausen. Symbolic model checking. In Alur and Henzinger [AH96], pages 419\u2013422."},{"issue":"1","key":"1_CR10","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/227595.227597","volume":"43","author":"W. Chen","year":"1996","unstructured":"W. Chen and D. S. Warren. Tabled evaluation with delaying for general logic programs. Journal of the ACM, 43(1):20\u201374, January 1996.","journal-title":"Journal of the ACM"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4), December 1996.","DOI":"10.1145\/242223.242257"},{"key":"1_CR12","unstructured":"D. Dams. Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology, 1996."},{"key":"1_CR13","unstructured":"E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the First Annual Symposium on Logic in Computer Science, pages 267\u2013278, 1986."},{"key":"1_CR14","unstructured":"M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In International Conference on Logic Programming, pages 1070\u20131080, 1988."},{"key":"1_CR15","first-page":"423","volume-title":"volume 1102 of Lecture Notes in Computer Science","author":"R. H. Hardin","year":"1996","unstructured":"R. H. Hardin, Z. Har'El, and R. P. Kurshan. COSPAN. In Alur and Henzinger [AH96], pages 423\u2013427."},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2), 1994.","DOI":"10.1006\/inco.1994.1045"},{"key":"1_CR17","first-page":"385","volume-title":"volume 1102 of Lecture Notes in Computer Science","author":"G. J. Holzmann","year":"1996","unstructured":"G. J. Holzmann and D. Peled. The state of SPIN. In Alur and Henzinger [AH96], pages 385\u2013389."},{"key":"1_CR18","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","volume-title":"Partial-Order Methods in Verification (POMIV '96)","year":"1996","unstructured":"G. Holzmann, D. Peled, and V. Pratt, editors. Partial-Order Methods in Verification (POMIV '96), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, New Brunswick, New Jersey, July 1996. American Mathematical Society."},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"J. Jaffar and J.-L. Lassez. Constraint logic programming. In ACM Symposium on Principles of Programming Languages, pages 111\u2013119, 1987.","DOI":"10.1145\/41625.41635"},{"key":"1_CR20","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u039c-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"J. W. Lloyd. Foundations of Logic Programming. Springer, 1984.","DOI":"10.1007\/978-3-642-96826-6"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"X. Liu, C. R. Ramakrishnan, and S. A. Smolka. Fully local and efficient evaluation of alternating fixed points. In Proceedings of the Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '98), Lecture Notes in Computer Science. Springer-Verlag, 1998.","DOI":"10.1007\/BFb0054161"},{"key":"1_CR23","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R. Milner","year":"1983","unstructured":"R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267\u2013310, 1983.","journal-title":"Theoretical Computer Science"},{"key":"1_CR24","unstructured":"R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989."},{"key":"1_CR25","unstructured":"I. Niemela and P. Simons. Efficient implementation of the well-founded and stable model semantics. In Joint International Conference and Symposium on Logic Programming, pages 289\u2013303, 1996."},{"key":"1_CR26","volume-title":"volume 137 of Lecture Notes in Computer Science","author":"J. P. Queille","year":"1982","unstructured":"J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proceedings of the International Symposium in Programming, volume 137 of Lecture Notes in Computer Science, Berlin, 1982. Springer-Verlag."},{"key":"1_CR27","volume-title":"Efficient model checking using tabled resolution","author":"Y. S. Ramakrishna","year":"1997","unstructured":"Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. W. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In Proceedings of the 9th International Conference on Computer-Aided Verification (CAV '97), Haifa, Israel, July 1997. Springer-Verlag."},{"key":"1_CR28","unstructured":"A. Roychoudhury, C. R. Ramakrishnan, I. V. Ramakrishnan, and S. A. Smolka. Tabulation-based induction proofs with applications to automated verification. In Workshop on Tabulation in Parsing and Deduction, 1998."},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"O. Sokolsky and S. A. Smolka. Local model checking for real-time systems. In Proceedings of the 7th International Conference on Computer-Aided Verification. American Mathematical Society, 1995.","DOI":"10.1007\/3-540-60045-0_52"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"K. Sagonas, T. Swift, and D. S. Warren. An abstract machine to compute fixed-order dynamically stratified programs. In International Conference on Automated Deduction (CADE), 1996.","DOI":"10.1007\/3-540-61511-3_98"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"H. Tamaki and T. Sato. OLDT resolution with tabulation. In International Conference on Logic Programming, pages 84\u201398. MIT Press, 1986.","DOI":"10.1007\/3-540-16492-8_66"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"A. van Gelder, K. A. Ross, and J. S. Schlipf. The well-founded semantics for general logic programs. Journal of the ACM, 38(3), 1991.","DOI":"10.1145\/116825.116838"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proc. 13th ACM Symp. on Principles of Programming, pages 184\u2013192, St. Petersburgh, January 1986.","DOI":"10.1145\/512644.512661"},{"key":"1_CR34","unstructured":"XSB. The XSB logic programming system v1.8, 1998. Available from http:\/\/www.cs.sunysb.edu\/~sbprolog."}],"container-title":["Lecture Notes in Computer Science","Principles of Declarative Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0056604","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T11:40:21Z","timestamp":1555760421000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0056604"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540650126","9783540497660"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/bfb0056604","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}