{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T14:26:25Z","timestamp":1742394385636},"publisher-location":"Berlin, Heidelberg","reference-count":20,"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_39","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:59:43Z","timestamp":1179586783000},"page":"485-499","source":"Crossref","is-referenced-by-count":30,"title":["Vacuum Cleaning CTL Formulae"],"prefix":"10.1007","author":[{"given":"Mitra","family":"Purandare","sequence":"first","affiliation":[]},{"given":"Fabio","family":"Somenzi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"39_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/3-540-63166-6_28","volume-title":"Ninth Conference on Computer Aided Verification (CAV\u201997)","author":"I. Beer","year":"1997","unstructured":"I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh. Efficient detection of vacuity in ACTL formulas. In O. Grumberg, editor, Ninth Conference on Computer Aided Verification (CAV\u201997), pages 279\u2013290. Springer-Verlag, Berlin, 1997. LNCS 1254."},{"key":"39_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/3-540-48683-6_21","volume-title":"Eleventh Conference on Computer Aided Verification (CAV\u201999)","author":"R. Bloem","year":"1999","unstructured":"R. Bloem, K. Ravi, and F. Somenzi. Efficient decision procedures for model checking of linear time logic properties. In N. Halbwachs and D. Peled, editors, Eleventh Conference on Computer Aided Verification (CAV\u201999), pages 222\u2013235. Springer-Verlag, Berlin, 1999. LNCS 1633."},{"key":"39_CR3","doi-asserted-by":"crossref","unstructured":"R. Bloem, K. Ravi, and F. Somenzi. Symbolic guided search for CTL model checking. In Proceedings of the Design Automation Conference, pages 29\u201334, Los Angeles, CA, June 2000.","DOI":"10.1145\/337292.337306"},{"key":"39_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Eighth Conference on Computer Aided Verification (CAV\u201996)","author":"R. K. Brayton","year":"1996","unstructured":"R. K. Brayton et al. VIS: A system for verification and synthesis. In T. Henzinger and R. Alur, editors, Eighth Conference on Computer Aided Verification (CAV\u201996), pages 428\u2013432. Springer-Verlag, Rutgers University, 1996. LNCS 1102."},{"issue":"8","key":"39_CR5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"39_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/3-540-44585-4_7","volume-title":"Thirteenth Conference on Computer Aided Verification (CAV\u201901)","author":"H. Chockler","year":"2001","unstructured":"H. Chockler, O. Kupferman, R. P. Kurshan, and M. Y. Vardi. A practical approach to coverage in model checking. In G. Berry, H. Comon, and A. Finkel, editors, Thirteenth Conference on Computer Aided Verification (CAV\u201901), pages 66\u201378. Springer-Verlag, Berlin, July 2001. LNCS 2102."},{"key":"39_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/3-540-45319-9_36","volume-title":"Tools and algorithms for the construction and analysis of systems (TACAS)","author":"H. Chockler","year":"2001","unstructured":"H. Chockler, O. Kupferman, and M. Y. Vardi. Coverage metrics for temporal logic model checking. In Tools and algorithms for the construction and analysis of systems (TACAS), pages 528\u2013542. Springer, 2001. LNCS 2031."},{"key":"39_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proceedings Workshop on Logics 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 Workshop on Logics of Programs, pages 52\u201371, Berlin, 1981. Springer-Verlag. LNCS 131."},{"key":"39_CR9","volume-title":"Model Checking","author":"E. M. Clarke","year":"1999","unstructured":"E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, Cambridge, MA, 1999."},{"key":"39_CR10","unstructured":"O. Coudert, C. Berthet, and J. C. Madre. Verification of sequential machines using Boolean functional vectors. In L. Claesen, editor, Proceedings IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pages 111\u2013128, Leuven, Belgium, November 1989."},{"key":"39_CR11","doi-asserted-by":"crossref","unstructured":"E. W. Dijkstra. Cooperating sequential processes. In Genuys, editor, Programming Languages, pages 43\u2013112. Academic Press, 1968.","DOI":"10.1007\/978-1-4757-3472-0_2"},{"key":"39_CR12","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/4317.001.0001","volume-title":"Logic Testing and Design for Testability","author":"H. Fujiwara","year":"1985","unstructured":"H. Fujiwara. Logic Testing and Design for Testability. MIT Press, Cambridge, MA, 1985."},{"key":"39_CR13","doi-asserted-by":"crossref","unstructured":"Y. Hoskote, T. Kam, P.-H. Ho, and X. Zhao. Coverage estimation for symbolic model checking. In Proceedings of the Design Automation Conference, pages 300\u2013305, New Orleans, LA, June 1999.","DOI":"10.1145\/309847.309936"},{"key":"39_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/3-540-48153-2_21","volume-title":"Correct Hardware Design and Verification Methods (CHARME\u201999)","author":"S. Katz","year":"1999","unstructured":"S. Katz, O. Grumberg, and D. Geist. \u201cHave I written enough properties?\u201d \u2014 A method of comparison between specification and implementation. In Correct Hardware Design and Verification Methods (CHARME\u201999), pages 280\u2013297, Berlin, September 1999. Springer-Verlag. LNCS 1703."},{"key":"39_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/3-540-48153-2_8","volume-title":"Correct Hardware Design and Verification Methods (CHARME\u201999)","author":"O. Kupferman","year":"1999","unstructured":"O. Kupferman and M. Y. Vardi. Vacuity detection in temporal model checking. In Correct Hardware Design and Verification Methods (CHARME\u201999), pages 82\u201396, Berlin, September 1999. Springer-Verlag. LNCS 1703."},{"key":"39_CR16","volume-title":"Computer-Aided Verification of Coordinating Processes","author":"R. P. Kurshan","year":"1994","unstructured":"R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994."},{"key":"39_CR17","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1994","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994."},{"key":"39_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-48153-2_19","volume-title":"Correct Hardware Design and Verification Methods (CHARME\u201999)","author":"K. Ravi","year":"1999","unstructured":"K. Ravi and F. Somenzi. Hints to accelerate symbolic traversal. In Correct Hardware Design and Verification Methods (CHARME\u201999), pages 250\u2013264, Berlin, September 1999. Springer-Verlag. LNCS 1703."},{"key":"39_CR19","unstructured":"D. Verkest, L. Claesen, and H. De Man. Special benchmark session on formal system design. In L. Claesen, editor, Proceedings IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pages 75\u201376, Leuven, Belgium, November 1989."},{"key":"39_CR20","unstructured":"URL: http:\/\/vlsi.colorado.edu\/~vis ."}],"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_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T05:21:01Z","timestamp":1556428861000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_39","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}