{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T22:58:24Z","timestamp":1765666704399},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540643562"},{"type":"electronic","value":"9783540697534"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054171","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:43:43Z","timestamp":1153979023000},"page":"167-183","source":"Crossref","is-referenced-by-count":31,"title":["A verified model checker for the modal \u039c-calculus in Coq"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Sprenger","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"H. R. Andersen. Verification of Temporal Properties of Concurrent Systems. PhD thesis, Computer Science Department, Aarhus University, June 1993.","DOI":"10.7146\/dpb.v22i445.6762"},{"key":"12_CR2","unstructured":"L. Augustsson, T. Coquand, and B. Nordstr\u00f6m. A short description of another logical framework. In G. Huet and P. G., editors, Preliminary Proceedings of Logical Frameworks, 1990."},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2: Background: Computational Structures, pages 118\u2013309. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"12_CR4","unstructured":"B. Barras. Coq en Coq. Technical Report 3026, INRIA, Oct. 1996."},{"key":"12_CR5","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, j.-C. Fili\u00e2tre, E. Gim\u00e9nez, H. Herbelin, G. Huet, and al. The Coq Proof Assistant Reference Manual, Version 6.1. Projet Coq, INRIA Rocquencourt, CNRS \u2014 ENS Lyon, Dec. 1996."},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/0304-3975(92)90183-G","volume":"96","author":"J. Bradfield","year":"1992","unstructured":"J. Bradfield and C. Stirling. Local model checking for infinite state spaces. Theoretical Computer Science, 96:157\u2013174, 1992.","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"12_CR7","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clarke","year":"1994","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512\u20131542, Sept. 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R. Cleaveland","year":"1990","unstructured":"R. Cleaveland. Tableau-based model checking in the propositional \u039c-calculus. Acta Informatica, 27:725\u2013747, 1990.","journal-title":"Acta Informatica"},{"key":"12_CR9","unstructured":"R. Cleaveland and B. Steffen. A preorder for partial process specifications. In CONCUR ' 90, volume 458 of Lecture Notes in Computer Science. Springer-Verlag, 1990."},{"key":"12_CR10","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95\u2013120, 1988.","journal-title":"Information and Computation"},{"issue":"2","key":"12_CR11","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2):253\u2013291, 1997.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"J. Dingel and T. Filkorn. Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In CAV '95, volume 939 of Lecture Notes in Computer Science. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60045-0_40"},{"key":"12_CR13","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambrdge Tracts in Theoretical Computer Science. Cambridge University Press, 1989."},{"key":"12_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, 1989.","DOI":"10.1145\/72981.72998"},{"key":"12_CR15","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and B. S. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:11\u201344, 1995.","journal-title":"Formal Methods in System Design"},{"key":"12_CR16","unstructured":"Z. Luo and R. Pollack. Lego proof development system: User's manual. Technical Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, 1992."},{"key":"12_CR17","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall International Series in Computer Science. Prentice Hall, 1989."},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"O. M\u00fcller and T. Nipkow. Combining model checking and deduction for I\/O-automata. In TACAS 95, volume 1019 of Lecture Notes in Computer Science, pages 1\u201316. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60630-0_1"},{"key":"12_CR19","unstructured":"C. Parent. Synth\u00e8se de preuves de programmes dans le Calcul des Constructions Inductives. PhD thesis, Ecole Normale Sup\u00e9rieure de Lyon, Jan. 1995."},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Extracting F\u03a9 programs from proofs in the Calculus of Constructions. In Sixteenth Annual ACM Symposium on the Priciples of Programming Languages, Austin, Texas, Jan. 1989.","DOI":"10.1145\/75277.75285"},{"key":"12_CR21","unstructured":"C Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. PhD thesis, Universit\u00e9 de Paris VII, Jan. 1989."},{"key":"12_CR22","volume-title":"Technical Report 92-49","author":"C. Paulin-Mohring","year":"1992","unstructured":"C. Paulin-Mohring. Inductive definitions in the system Coq \u2014 rules and properties. Technical Report 92-49, Laboratoire de l'Informatique du Parall\u00e9lisme, ENS Lyon, France, Dec. 1992."},{"key":"12_CR23","first-page":"1","volume":"11","author":"C. Paulin-Mohring","year":"1993","unstructured":"C. Paulin-Mohring and B. Werner. Synthesis of ML programs in the system coq. Journal of Symbolic Computation, 11:1\u201334, 1993.","journal-title":"Journal of Symbolic Computation"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"S. Rajan, N. Shankar, and M. K. Srivas. An integration of model checking with automated proof checking. In CAV '95, volume 939 of Lecture Notes in Computer Science, pages 84\u201397. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60045-0_42"},{"key":"12_CR25","volume-title":"PhD thesis","author":"B. Werner","year":"1994","unstructured":"B. Werner. Une Th\u00e9orie des Constructions Inductives. PhD thesis, Universit\u00e9 de Paris 7, France, 1994."},{"key":"12_CR26","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/0304-3975(91)90043-2","volume":"83","author":"G. Winskel","year":"1991","unstructured":"G. Winskel. A note on model checking the modal \u039c-calculus. Theoretical Computer Science, 83:157\u2013167, 1991.","journal-title":"Theoretical Computer Science"},{"key":"12_CR27","doi-asserted-by":"crossref","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. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_6"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"S. Yu and Z. Luo. Implementing a model checker for LEGO. In Formal Methods Europe, 1997.","DOI":"10.1007\/3-540-63533-5_23"}],"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\/BFb0054171","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,5]],"date-time":"2024-02-05T15:47:46Z","timestamp":1707148066000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0054171"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643562","9783540697534"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/bfb0054171","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}