{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,25]],"date-time":"2026-10-25T14:21:53Z","timestamp":1792938113731,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540423454","type":"print"},{"value":"9783540445852","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44585-4_2","type":"book-chapter","created":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T14:39:50Z","timestamp":1265899190000},"page":"2-13","source":"Crossref","is-referenced-by-count":91,"title":["Certifying Model Checkers"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"APR+01._T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck. Parameterized verification with automatically computed inductive assertions. In CAV, 2001.","DOI":"10.1007\/3-540-44585-4_19"},{"key":"2_CR2","unstructured":"BBC+00._N. Bjorner, A. Browne, M. Col\u00f3n, B. Finkbeiner, Z. Manna, H. Sipma, and T. Uribe. Verifying temporal properties of reactive systems: A STeP tutorial. Formal Methods in System Design, 2000."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"J. Bradfield and C. Stirling. Local model checking for infinite state spaces. TCS, 96, 1992.","DOI":"10.1016\/0304-3975(92)90183-G"},{"key":"2_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","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 Workshop on Logics of Programs, volume 131 of LNCS, 1981."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"S.A. Cook. Soundness and completeness of an axiom system for program verification. SIAM J. Comput, 1978.","DOI":"10.1137\/0207005"},{"key":"2_CR7","unstructured":"E.A. Emerson and C.S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In FOCS, 1991."},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"E. Allen Emerson, C.S. Jutla, and A.P. Sistla. On model-checking for fragments of \u00b5-calculus. In CAV, 1993.","DOI":"10.1007\/3-540-56922-7_32"},{"key":"2_CR9","unstructured":"E.A. and C-L. Lei. Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In LICS, 1986."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science: Volume B, Formal Models and Semantics. North-Holland Pub. Co.\/MIT Press, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"L. Fix and O. Grumberg. Verification of temporal properties. Journal of Logic and Computation, 1996.","DOI":"10.1093\/logcom\/6.3.343"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"R. Floyd. Assigning meaning to programs. In Mathematical Aspects of Computer Science XIX. American Mathemetical Society, 1967.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"2_CR13","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"R.H. Hardin","year":"1996","unstructured":"R.H. Hardin, Z. Har'el, and R.P. Kurshan. COSPAN. In CAV, volume 1102 of LNCS, 1996."},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 1969.","DOI":"10.1145\/363235.363259"},{"key":"2_CR15","series-title":"Lect Notes Comput Sci","volume-title":"HUG","author":"J.J. Joyce","year":"1993","unstructured":"J.J. Joyce and C-J.H. Seger. The HOL-Voss system: Model-checking inside a general-purpose theorem-prover. In HUG, volume 780 of LNCS, 1993."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"D. Janin and I. Walukiewicz. Automata for the modal mu-calulus and related results. In MFCS, 1995.","DOI":"10.7146\/brics.v2i27.19929"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"R.M. Keller. Formal verification of parallel programs. CACM, 1976.","DOI":"10.1145\/360248.360251"},{"key":"2_CR18","unstructured":"A. Kick. Generation of witnesses for global mu-calculus model checking. available at http:\/\/liinwww.ira.uka.de\/~kick"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"D. Kozen. Results on the propositional mu-calculus. In ICALP, 1982.","DOI":"10.7146\/dpb.v11i146.7420"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Verification of infinite state systems by compositional model checking. In CHARME, 1999.","DOI":"10.1007\/3-540-48153-2_17"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"P. Manolios, K.S. Namjoshi, and R. Summers. Linking theorem proving and model-checking with well-founded bisimulation. In CAV, 1999.","DOI":"10.1007\/3-540-48683-6_32"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. How to cook a temporal proof system for your pet language. In POPL, 1983.","DOI":"10.1145\/567067.567082"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Specification and verification of concurrent programs by 8-automata. In POPL, 1987.","DOI":"10.1145\/41625.41626"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"G.C. Necula and P. Lee. Safe kernel extensions without run-time checking. In OSDI, 1996.","DOI":"10.1145\/238721.238781"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"G.C. Necula and P. Lee. The design and implementation of a certifying compiler. In PLDI, 1998.","DOI":"10.1145\/277650.277752"},{"key":"2_CR26","series-title":"Lect Notes Comput Sci","volume-title":"TACAS","author":"A. Pnueli","year":"2001","unstructured":"A. Pnueli, S. Ruah, and L. Zuck. Automatic deductive verification with invisible invariants. In TACAS, volume 2031 of LNCS, 2001."},{"key":"2_CR27","series-title":"Lect Notes Comput Sci","volume-title":"From model checking to a temporal proof","author":"D. Peled","year":"2001","unstructured":"D. Peled and L. Zuck. From model checking to a temporal proof. In The 8th International SPIN Workshop on Model Checking of Software, volume 2057 of LNCS, 2001."},{"key":"2_CR28","series-title":"Lect Notes Comput Sci","volume-title":"Specification and verification of concurrent systems in CESAR","author":"J.-P. Queille","year":"1982","unstructured":"J-P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. of the 5th International Symposium on Programming, volume 137 of LNCS, 1982."},{"key":"2_CR29","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, volume 939 of LNCS, 1995."},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"R.S. Streett and E.A. Emerson. The propositional mu-calculus is elementary. In ICALP, 1984. Full version in Information and Computation 81(3): 249\u2013264, 1989.","DOI":"10.1016\/0890-5401(89)90031-X"},{"key":"2_CR31","series-title":"Lect Notes Comput Sci","volume-title":"TACAS","author":"C. Sprenger","year":"1998","unstructured":"C. Sprenger. A verified model checker for the modal \u00b5-calculus in Coq. In TACAS, volume 1384 of LNCS, 1998."},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"P. Stevens and C. Stirling. Practical model-checking using games. In TACAS, 1998.","DOI":"10.1007\/BFb0054166"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"C. Stirling and D. Walker. Local model checking in the modal mu-calculus. In TAPSOFT, 1989. Full version in TCS vol.89, 1991.","DOI":"10.1016\/0304-3975(90)90110-4"},{"key":"2_CR34","series-title":"Lect Notes Comput Sci","volume-title":"FME","author":"S. Yu","year":"1997","unstructured":"S. Yu and Z. Luo. Implementing a model checker for LEGO. In FME, volume 1313 of LNCS, 1997."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44585-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T18:29:58Z","timestamp":1558808998000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44585-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423454","9783540445852"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-44585-4_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}