{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:20:44Z","timestamp":1725664844107},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540635338"},{"type":"electronic","value":"9783540695936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63533-5_23","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:29:07Z","timestamp":1330298947000},"page":"442-458","source":"Crossref","is-referenced-by-count":8,"title":["Implementing a model checker for LEGO"],"prefix":"10.1007","author":[{"given":"Shenwei","family":"Yu","sequence":"first","affiliation":[]},{"given":"Zhaohui","family":"Luo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"23_CR1","unstructured":"L. Augustsson, Th. Coquand, and B. Nordstr\u00f6m. A short description of another logical framework. In G. Huet and G. Plotkin, editors, Preliminary Proc. of Logical Frameworks, 1990."},{"key":"23_CR2","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/0304-3975(92)90183-G","volume":"96","author":"J. Bradfield","year":"1992","unstructured":"Julian Bradfield and Colin Stirling. Local model checking for inifinite state spaces. Theoretical Computer Science, 96:157\u2013174, 1992.","journal-title":"Theoretical Computer Science"},{"key":"23_CR3","unstructured":"Glenn Bruns. Algebraic Abstraction with Process Preorders. in preparation, 1995."},{"issue":"2","key":"23_CR4","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computation"},{"key":"23_CR5","series-title":"volume 818 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Proc. 6th Conference on Computer Aided Verification","author":"E.M. Clarke","year":"1994","unstructured":"E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In D.L. Dill, editor, Proc. 6th Conference on Computer Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 415\u2013427, Stanford, CA, June 1994. Springer Verlag."},{"key":"23_CR6","unstructured":"R. L. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Pretice-Hall, 1986."},{"key":"23_CR7","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. G. Bruijn de","year":"1972","unstructured":"Nicolaas G. de Bruijn. Lamda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Math., 34:381\u2013392, 1972.","journal-title":"Indag. Math."},{"key":"23_CR8","unstructured":"G. Dowek et al. The Coq Proof Assistent: User's Guide (version 5.6). INRIA-Rocquencourt and CNRS-ENS Lyon, 1991."},{"key":"23_CR9","first-page":"84","volume-title":"Proceedings of the 10th Symposium on Principles of Programming Languages","author":"E.A. Emerson","year":"1985","unstructured":"E.A. Emerson and C.L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the 10th Symposium on Principles of Programming Languages, pages 84\u201396, New Orleans, LA, January 1985. Association for Computing Machinery."},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Urban Engberg, Peter Gronning, and Leslie Lamport. Mechanical verification of concurrent systems with TLA. In G.V. Bochmann and D.K. Probst, editors, Computer-Aided Verification 92, volume 663 of Lecture Notes in Computer Science, pages 44\u201355. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-56496-9_5"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Jeffrey J. Joyce and Carl-Johan H. Seger. Linking Bdd-based symbolic evaluation to interactive theorem proving. In Proceedings of the 30th Design Automation Conference. Association for Computing Machinery, 1993.","DOI":"10.1145\/157485.164981"},{"key":"23_CR12","series-title":"volume 697 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-56922-7_14","volume-title":"Computer-Aided Verification 93","author":"R. Kurshan","year":"1993","unstructured":"R. Kurshan and L. Lamport. Verification of a multiplier: 64 bits and beyond. In Costas Courcoubetis, editor, Computer-Aided Verification 93, volume 697 of Lecture Notes in Computer Science, pages 166\u2013179, Elounda, Greece, June\/July 1993. Springer Verlag."},{"key":"23_CR13","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R. P. Kurshan","year":"1994","unstructured":"Robert P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton, New Jersey, 1994."},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan and K. McMillan. A structural induction theorem for processes. In 8th ACM Symposium on Principles of Distributed Computing, pages 239\u2013248, Edmonton, Albera, Canada, August 1989.","DOI":"10.1145\/72981.72998"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"23_CR16","unstructured":"Z. Luo and R. Pollack. LEGO Proof Development System: User's Manual. LFCS Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, 1992."},{"key":"23_CR17","unstructured":"L. Magnusson. The new implementation of ALF. In Informal Proceedings of Workshop on Logical Frameworks, Bastad, 1992."},{"key":"23_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1993","unstructured":"Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1993."},{"key":"23_CR19","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, 1989."},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Olaf Milller and Tobias Nipkow. Combining Model Checking and Deduction for I\/O-Automata. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1019 of Lecture Notes in Computer Science, pages 1\u201316. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60630-0_1"},{"key":"23_CR21","series-title":"volume 607 of Lecture Notes in Artificial Intelligence","first-page":"748","volume-title":"11th International Conference on Automted Deduction(CADE)","author":"S. Owre","year":"1992","unstructured":"S. Owre, J.M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automted Deduction(CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748\u2013752, Saratoga, NY, June 1992. Springer-Verlag."},{"key":"23_CR22","unstructured":"Randy Pollack. Incremental Changes in LEGO: 1994, May 1994. Available by ftp with LEGO distribution."},{"key":"23_CR23","series-title":"volume 902 of Lecture Notes in Computer Science","volume-title":"Proceedings of the Second International Conference on Typed Lambda Calculi and Applications","author":"R. Pollack","year":"1995","unstructured":"Robert Pollack. A Verified Typechecker. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, Edinburgh, 1995. Springer-Verlag."},{"key":"23_CR24","series-title":"volume 939 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Computer Aided Verification, Proc. 7th Int. Conference","author":"S. Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, and M. K. Srivas. An Integration of Model Checking with Automated Proof checking. In Computer Aided Verification, Proc. 7th Int. Conference, volume 939 of Lecture Notes in Computer Science, pages 84\u201397, Li\u00e8ge, Belgium, July 1995. Springer-Verlag."},{"key":"23_CR25","doi-asserted-by":"crossref","unstructured":"Glynn Winskel. A note on model checking the modal v-calculus. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, Proceedings of ICALP, volume 372 of Lecture Notes in Computer Science, pages 761\u2013772. Springer-Verlag, 1989.","DOI":"10.1007\/BFb0035797"},{"key":"23_CR26","series-title":"volume 407 of Lecture Notes in Computer Science","first-page":"68","volume-title":"International Workshop on 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 J. Sifakis, editor, International Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 68\u201380, Grenoble, France, June 1989. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","FME '97: Industrial Applications and Strengthened Foundations of Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63533-5_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T18:15:09Z","timestamp":1713636909000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63533-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540635338","9783540695936"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-63533-5_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}