{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T12:18:15Z","timestamp":1767183495967,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631668"},{"type":"electronic","value":"9783540691952"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63166-6_28","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:13:43Z","timestamp":1330298023000},"page":"279-290","source":"Crossref","is-referenced-by-count":51,"title":["Efficient detection of vacuity in ACTL formulas"],"prefix":"10.1007","author":[{"given":"Ilan","family":"Beer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shoham","family":"Ben-David","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cindy","family":"Eisner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoav","family":"Rodeh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"D. Beatty and R. Bryant, \u201cFormally verifying a microprocessor using a simulation methodology\u201d, Design Automation Conference '94, pp. 596\u2013602.","DOI":"10.1145\/196244.196575"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, A. Landver, \u201cRuleBase: an Industry-Oriented Formal Verification Tool\u201d, in Proc. 33 rd Design Automation Conference 1996, pp. 655\u2013660.","DOI":"10.1145\/240518.240642"},{"key":"28_CR3","first-page":"52","volume-title":"Lecture Notes in Computer Science, Vol. 131","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson, \u201cDesign and synthesis of synchronization skeletons using Branching Time Temporal Logic\u201d, in Proc. Workshop on Logics of Programs, Lecture Notes in Computer Science, Vol. 131 (Springer, Berlin, 1981) pp. 52\u201371."},{"key":"28_CR4","unstructured":"E.M. Clark and E.A. Emerson, \u201cCharacterizing Properties of Parallel Programs as Fixed-point\u201d, in Seventh International Colloquium on Automata, Languages, and Programming, Volume 85 of LNCS, 1981."},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, K. McMillan, X. Zhao, \u201cEfficient Generation of Counterexamples and Witnesses in Symbolic Model Checking\u201d, Design Automation Conference 1995, pp. 427\u2013432.","DOI":"10.1145\/217474.217565"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"O. Grumberg and D. Long, \u201cModel checking and modular verification.\u201d In J.C.M. Baeten and J.F. Groote, editors, Proccedings of CONCUR '91: 2nd International Conference on Concurrency Theory, Volume 527 of LNCS, 1991.","DOI":"10.1007\/3-540-54430-5_93"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"R. Hojati, R.K. Brayton and R.P. Kurshan, \u201cBDD-based debugging of designs using language containment and fair CTL.\u201d CAV '93, pp. 41\u201358.","DOI":"10.1007\/3-540-56922-7_5"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"R. Kurshan, \u201cAnalysis of Discrete Event Coordination,\u201d LNCS 1990.","DOI":"10.1007\/3-540-52559-9_74"},{"key":"28_CR9","unstructured":"D. Long, \u201cModel Checking, Abstraction and Compositional Verification\u201d, Ph.D. Thesis, CMU, 1993."},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, \u201cSymbolic Model Checking\u201d, Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"B. Plessier and C. Pixley, \u201cFormal Verification of a Commercial Serial Bus Interface\u201d, International Phoenix Conference on Computers and Communications, 1995, pp. 378\u2013382.","DOI":"10.1109\/PCCC.1995.472465"},{"key":"28_CR12","unstructured":"G. Shurek, O. Grumberg, \u201cThe Computer-Aided Modular Framework \u2014Motivation, Solutions and Evaluation Criteria\u201d, Workshop on Computer Aided Verification, 1990."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63166-6_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:39:12Z","timestamp":1742600352000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63166-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631668","9783540691952"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-63166-6_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}