{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T07:09:06Z","timestamp":1794380946004,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540223429","type":"print"},{"value":"9783540278139","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27813-9_5","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T00:57:57Z","timestamp":1284425877000},"page":"57-69","source":"Crossref","is-referenced-by-count":19,"title":["An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-540-45069-6_35","volume-title":"Computer Aided Verification","author":"R. Armoni","year":"2003","unstructured":"Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A.: Enhanced vacuity detection in linear temporal logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 368\u2013380. Springer, Heidelberg (2003)"},{"key":"5_CR2","volume-title":"31st DAC","author":"D. Beatty","year":"1994","unstructured":"Beatty, D., Bryant, R.: Formally verifying a microprocessor using a simulation methodology. In: 31st DAC, IEEE Computer Society Press, Los Alamitos (1994)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Beer","year":"1997","unstructured":"Beer, S., Ben-David, C.: Efficient detection of vacuity in ACTL formulas. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, Springer, Heidelberg (1997) ; Full version in FMSD,18(2) (2001)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-44585-4_7","volume-title":"Computer Aided Verification","author":"H. Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Kurshan, R.P., Vardi, M.Y.: A practical approach to coverage in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 66. Springer, Heidelberg (2001)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, Springer, Heidelberg (1982)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-45719-4_11","volume-title":"Algebraic Methodology and Software Technology","author":"Y. Dong","year":"2002","unstructured":"Dong, Y., Sarna-Starosta, B., Ramakrishnan, C.R., Smolka, S.A.: Vacuity checking in the modal mu-calculus. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, p. 147. Springer, Heidelberg (2002)"},{"issue":"1","key":"5_CR7","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: Sometimes and Not Never revisited: on Branching versus Linear Time Temporal Logic. J. ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. In: Leeuwen, J. v. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B: Formal Methods and Semantics, Elsevier and MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"5_CR9","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy (extended abstract). In: FOCS (1991)"},{"key":"5_CR10","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In: LICS (1986)"},{"key":"5_CR11","volume-title":"PSTV","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV, Chapman & Hall, Boca Raton (1995)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019el, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, Springer, Heidelberg (1996)"},{"key":"5_CR13","volume-title":"37th DAC","author":"Y. Hoskote","year":"1999","unstructured":"Hoskote, Y., Kam, T., Ho, P.-H., Zhao, X.: Coverage estimation for symbolic model checking. In: 37th DAC, ACM Press, New York (1999)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_21","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Katz","year":"1999","unstructured":"Katz, S., Geist, D., Grumberg, O.: Have I written enough properties? A method for comparison between specification and implementation. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, Springer, Heidelberg (1999)"},{"key":"5_CR15","unstructured":"Kick, A.: Generation of witnesses for global mu-calculus model checking (1995), available at http:\/\/citeseer.ist.psu.edu\/kick95generation.html"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0025769","volume-title":"ICALP","author":"D. Kozen","year":"1982","unstructured":"Kozen, D.: Results on the propositional mu-calculus. In: ICALP. LNCS, vol.\u00a0140, Springer, Heidelberg (1982)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-48153-2_8","volume-title":"Correct Hardware Design and Verification Methods","author":"O. Kupferman","year":"1999","unstructured":"Kupferman, O., Y. Vardi, M.: Vacuity detection in temporal model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 82\u201398. Springer, Heidelberg (1999)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. STTT\u00a04(2) (2003)","DOI":"10.1007\/s100090100062"},{"key":"5_CR19","unstructured":"Maidl, M.: The common fragment of CTL and LTL. In: FOCS (2000)"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Specification and verification of concurrent programs by \u2200-automata. In: POPL (1987)","DOI":"10.1145\/41625.41626"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-44585-4_2","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2001","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 2. Springer, Heidelberg (2001)"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-45294-X_25","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"D.A. Peled","year":"2001","unstructured":"Peled, D.A., Pnueli, A., Zuck, L.D.: From falsification to verification. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, p. 292. Springer, Heidelberg (2001)"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/3-540-45657-0_39","volume-title":"Computer Aided Verification","author":"M. Purandare","year":"2002","unstructured":"Purandare, M., Somenzi, F.: Vacuum cleaning CTL formulae. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 485. Springer, Heidelberg (2002)"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/BFb0054166","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Stevens","year":"1998","unstructured":"Stevens, P., Stirling, C.: Practical model-checking using games. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, p. 85. Springer, Heidelberg (1998)"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","volume-title":"FME \u201997 Industrial Applications and Strengthened Foundations of Formal Methods","author":"S. Yu","year":"1997","unstructured":"Yu, S., Luo, Z.: Implementing a model checker for LEGO. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol.\u00a01313, Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27813-9_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:22:07Z","timestamp":1605741727000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27813-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223429","9783540278139"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27813-9_5","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/b98490","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}