{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:24:48Z","timestamp":1745994288835},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439974"},{"type":"electronic","value":"9783540456575"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_37","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:59:43Z","timestamp":1179586783000},"page":"455-470","source":"Crossref","is-referenced-by-count":30,"title":["Evidence-Based Model Checking"],"prefix":"10.1007","author":[{"given":"Li","family":"Tan","sequence":"first","affiliation":[]},{"given":"Rance","family":"Cleaveland","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"issue":"1","key":"37_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"H. R. Andersen","year":"1994","unstructured":"H. R. Andersen. Model checking and boolean graphs. Theoretical Computer Science, 126(1):3\u201330, April 1994.","journal-title":"Theoretical Computer Science"},{"key":"37_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Ninth International Conference on Computer Aided Verification (CAV\u2019 97)","author":"I. Beer","year":"1997","unstructured":"I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh. Efficient detection of vacuity in ACTL formulas. In Proceedings of the Ninth International Conference on Computer Aided Verification (CAV\u2019 97), LNCS 1254. Springer-Verlag, 1997."},{"key":"37_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 96)","author":"G. S. Bhat","year":"1996","unstructured":"G. S. Bhat and R. Cleaveland. Efficient local model checking for fragments of the modal \u03bc-calculus. In Proceedings of the Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 96), LNCS 1055. Springer-Verlag, March 1996."},{"key":"37_CR4","doi-asserted-by":"crossref","unstructured":"G. S. Bhat and R. Cleaveland. Efficient model checking via the equational \u03bc-calculus. In E. M. Clarke, editor, 11th Annual Symposium on Logic in Computer Science (LICS\u2019 96), pages 304\u2013312, New Brunswick, NJ, July 1996. Computer Society Press.","DOI":"10.1109\/LICS.1996.561358"},{"key":"37_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Seventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 01)","author":"G. Bhat","year":"2001","unstructured":"G. Bhat, R. Cleaveland, and A. Groce. Efficient model checking via b\u00fcchi tableau automaton. In Proceedings of the Seventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 01), LNCS 2031. Springer-Verlag, 2001."},{"key":"37_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Workshop on Logic of Programs","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 Proceedings of the Workshop on Logic of Programs, Yorktown Heights, volume 131 of Lecture Notes in Computer Science. Springer-Verlag, 1981."},{"key":"37_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":"37_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0016951","volume-title":"Proc. 32nd Design Automaton Conference","author":"E. Clarke","year":"1995","unstructured":"E. Clarke, O. Grumberg, K. McMillian, and X. Zhao. Efficent generation of counterexamples and witnesses in symbolic model checking. In Proc. 32nd Design Automaton Conference, San Francisco, CA, 1995. [CKV01] H. Chockler, O. Kupferman, and M. Vardi. Coverage metrics for temporal logic model checking. In Proceedings of the Seventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 01), LNCS 2031. Springer-Verlag, April 2001."},{"key":"37_CR9","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland and B. U. Steffen. A linear-time model checking algorithm for the alternation-free modal mu-calculus. Formal Methods in System Design, 2:121\u2013147, 1993.","journal-title":"Formal Methods in System Design"},{"key":"37_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/3-540-61474-5_87","volume-title":"Computer Aided Verification (CAV\u2019 96)","author":"R. Cleaveland","year":"1996","unstructured":"R. Cleaveland and S. Sims. The NCSU concurrency workbench. In R. Alur and T. A. Henzinger, editors, Computer Aided Verification (CAV\u2019 96), volume 1102 of Lecture Notes in Computer Science, pages 394\u2013397, New Brunswick, New Jersey, July 1996. Springer-Verlag."},{"key":"37_CR11","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M. Dam","year":"1994","unstructured":"M. Dam. CTL* and ECTL* as fragement of the modal \u03bc-calculus. Theoretical Computer Science, 126:77\u201396, 1994.","journal-title":"Theoretical Computer Science"},{"key":"37_CR12","unstructured":"E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Symposium on Logic in Computer Science (LICS\u2019 86), pages 267\u2013278, Cambridge, Massachusetts, June 1986. Computer Society Press."},{"key":"37_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45315-6_18","volume-title":"The 4th International Conference on Foundations of Software Science and Computation Structures","author":"V. King","year":"2001","unstructured":"V. King, O. Kupferman, and M. Y. Vardi. On the complexity of parity word automaton. In The 4th International Conference on Foundations of Software Science and Computation Structures, Vol. 2030 of Lecture Notes in Computer Science, 2001."},{"key":"37_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Tenth Conference on Correct Hardware Design and Verification Mothods","author":"O. Kupferman","year":"1999","unstructured":"O. Kupferman and M. Y. Vardi. Vacuity detection in temporal model checking. In Proceedings of the Tenth Conference on Correct Hardware Design and Verification Mothods, LNCS 1703, 1999."},{"issue":"2","key":"37_CR15","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"O. Kupferman, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312\u2013360, March 2000.","journal-title":"Journal of the ACM"},{"key":"37_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 98)","author":"X. Liu","year":"1998","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\u2019 98), LNCS1389. Springer-Verlag, 1998."},{"key":"37_CR17","unstructured":"A. Mader. Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, M\u00fcchen, Techn-Univ., 1997."},{"key":"37_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46419-0_18","volume-title":"Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 00)","author":"R. Mateescu","year":"2000","unstructured":"R. Mateescu. Efficient diagnostic generation for boolean equation system. In Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 00), Vol. 1785 of Lecture Notes in Computer Science. Springer-Verlag, March 2000."},{"key":"37_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 13th International Conference on Computer Aided Verification (CAV\u2019 01)","author":"K. Namjoshi","year":"2001","unstructured":"K. Namjoshi. Certifying model checkers. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV\u2019 01), LNCS 2102. Springer-Verlag, 2001."},{"key":"37_CR20","series-title":"Lect Notes Comput Sci","volume-title":"FST&TCS","author":"D. Peled","year":"2001","unstructured":"D. Peled, A. Pnueli, and L. Zuck. From falsification to verification. In FST&TCS, volume 2245 of Lecture Notes in Computer Science. Springer-Verlag, 2001."},{"key":"37_CR21","series-title":"Lect Notes Comput Sci","volume-title":"SPIN","author":"D. Peled","year":"2001","unstructured":"D. Peled and L. Zuck. From model checking to a temporal proof. In M. Dwyer, editor, SPIN 2001, volume 2057 of Lecture Notes in Computer Science, pages 1\u201314, Toronto, May 2001. Springer-Verlag."},{"key":"37_CR22","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the International Symposium in Programming","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":"37_CR23","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 98)","author":"P. Stevens","year":"1998","unstructured":"P. Stevens and C. Stirling. Practical model checking using games. In Proceedings of the Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 98), LNCS1389. Springer-Verlag, 1998."},{"key":"37_CR24","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Sixth International Conference on Concurrency Theory (CONCUR\u2019 95)","author":"C. Stirling","year":"1995","unstructured":"C. Stirling. Local model checking games. In I. Lee and S. A. Smolka, editors, Proceedings of the Sixth International Conference on Concurrency Theory (CONCUR\u2019 95), Vol. 962 of Lecture Notes in Computer Science. Springer-Verlag, 1995."},{"key":"37_CR25","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/0020-0190(82)90136-3","volume":"14","author":"R. E. Tarjan","year":"1982","unstructured":"R. E. Tarjan. A hierarchical clusting algorithm using strong components. Information Processing Letters, 14:26\u201329, 1982.","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T05:21:12Z","timestamp":1556428872000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_37","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}