{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:50:26Z","timestamp":1742392226014},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540418658"},{"type":"electronic","value":"9783540453192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45319-9_36","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T15:50:47Z","timestamp":1184601047000},"page":"528-542","source":"Crossref","is-referenced-by-count":28,"title":["Coverage Metrics for Temporal Logic Model Checking"],"prefix":"10.1007","author":[{"given":"Hana","family":"Chockler","sequence":"first","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"D. Beaty and R. Bryant. Formally verifying a microprocessor using a simulation methodology. In Proc. 31st DAC, pp. 596\u2013602. IEEE Computer Society, 1994.","key":"36_CR1","DOI":"10.1145\/196244.196575"},{"key":"36_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/3-540-63166-6_28","volume-title":"Proc. 9th CAV","author":"I. Beer","year":"1997","unstructured":"I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh. Efficient detection of vacuity in ACTL formulas. In Proc. 9th CAV, LNCS 1254, pp. 279\u2013290, 1997."},{"key":"36_CR3","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115\u2013131, 1988.","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"J.P. Bergmann and M.A. Horowitz. Improving coverage analysis and test generation for large designs. In IEEE Int. Conf. for CAD, pp. 580\u2013584, 1999.","key":"36_CR4","DOI":"10.1109\/ICCAD.1999.810714"},{"key":"36_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proc. 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 Proc. Workshop on Logic of Programs, LNCS 131, pp. 52\u201371. Springer-Verlag, 1981."},{"doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, K.L. McMillan, and X. Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proc. 32nd DAC, pp. 427\u2013432. IEEE Computer Society, 1995.","key":"36_CR6","DOI":"10.1145\/217474.217565"},{"unstructured":"E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.","key":"36_CR7"},{"doi-asserted-by":"crossref","unstructured":"K.-T. Cheng and A. Krishnakumar. Automatic functional test generation using the extended finite state machine model. In Proc. 30th DAC, pp. 86\u201391, 1993.","key":"36_CR8","DOI":"10.1145\/157485.164585"},{"doi-asserted-by":"crossref","unstructured":"S. Devadas, A. Ghosh, and K. Keutzer. An observability-based code coverage metric for functional simulation. In Proc. CAD, pp. 418\u2013425, 1996.","key":"36_CR9","DOI":"10.1109\/ICCAD.1996.569832"},{"doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Temporal andmodal logic. Handbook of TheoreticalComputer Science, pp. 997\u20131072, 1990.","key":"36_CR10","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"doi-asserted-by":"crossref","unstructured":"F. Fallah, P. Ashar, and S. Devadas. Simulation vector generation from hdl descriptions for observability enhanced-statement coverage. In Proc. 36th DAC, pp. 666\u2013671, 1999.","key":"36_CR11","DOI":"10.1145\/309847.310023"},{"doi-asserted-by":"crossref","unstructured":"F. Fallah, S. Devadas, and K. Keutzer. OCCOM: Efficient Computation of Observability-Based Code Coverage Metrics for Functional Simulation. In Proc. 35th DAC, pp. 152\u2013157, 1998.","key":"36_CR12","DOI":"10.1145\/277044.277078"},{"doi-asserted-by":"crossref","unstructured":"R.C. Ho and M.A. Horowitz. Validation coverage analysis for complex digital designs. In Proc. CAD, pp. 146\u2013151, 1996.","key":"36_CR13","DOI":"10.1109\/ICCAD.1996.569537"},{"doi-asserted-by":"crossref","unstructured":"Y. Hoskote, T. Kam, P.-H Ho, and X. Zhao. Coverage estimation for symbolic model checking. In Proc. 36th DAC, pp. 300\u2013305, 1999.","key":"36_CR14","DOI":"10.1145\/309847.309936"},{"doi-asserted-by":"crossref","unstructured":"Y. Hoskote, D. Moundanos, and J. Abraham. Automatic extraction of the control flow machine and application to evaluating coverage of verification vectors. In Proc. ICDD, pp. 532\u2013537, 1995.","key":"36_CR15","DOI":"10.1109\/ICCD.1995.528919"},{"doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.","key":"36_CR16","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"36_CR17","first-page":"477","volume":"F-13","author":"D. Harel","year":"1985","unstructured":"D. Harel and A. Pnueli. On the development of reactive systems. NATO Advanced Summer Institutes, volume F-13, pp. 477\u2013498. Springer-Verlag, 1985.","journal-title":"NATO Advanced Summer Institutes"},{"key":"36_CR18","volume-title":"Logic Synthesis and Verification Algorithms","author":"G.D. Hachtel","year":"1996","unstructured":"G.D. Hachtel and F. Somenzi. Logic Synthesis and Verification Algorithms. Kluwer Academic Publishers, MA, 1996."},{"doi-asserted-by":"crossref","unstructured":"R. Ho, C. Yang, M. Horowitz, and D. Dill. Architecture validation for processors. In Proc. of the 22nd Annual Symp. on Comp. Arch., pp. 404\u2013413, 1995.","key":"36_CR19","DOI":"10.1145\/223982.224450"},{"key":"36_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/3-540-48153-2_21","volume-title":"10th CHARME","author":"S. Katz","year":"1999","unstructured":"S. Katz, D. Geist, and O. Grumberg. \u201cHave I written enough properties?\u201d a method of comparison between specification and implementation. In 10th CHARME, LNCS 1703, pp. 280\u2013297. Springer-Verlag, 1999."},{"doi-asserted-by":"crossref","unstructured":"M. Kantrowitz and L. Noack. I\u2019m done simulating: Now what? verification coverage analysis and correctness checking of the dec chip 21164 alpha microprocessor. In Proc. of DAC, pp. 325\u2013330, 1996.","key":"36_CR21","DOI":"10.1109\/DAC.1996.545595"},{"unstructured":"R.P. Kurshan. FormalCheck User\u2019s Manual. Cadence Design, Inc., 1998.","key":"36_CR22"},{"key":"36_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/3-540-48153-2_8","volume-title":"10th CHARME","author":"O. Kupferman","year":"1999","unstructured":"O. Kupferman and M.Y. Vardi. Vacuity detection in temporal model checking. In 10th CHARME, LNCS 1703. pp. 82\u201396, Springer-Verlag, 1999."},{"issue":"2","key":"36_CR24","doi-asserted-by":"publisher","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, 2000.","journal-title":"Journal of the ACM"},{"doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th POPL, pp. 97\u2013107, 1985.","key":"36_CR25","DOI":"10.1145\/318593.318622"},{"doi-asserted-by":"crossref","unstructured":"D. Moumdanos, J.A. Abraham, and Y.V. Hoskote. Abstraction techniques for validation coverage analysis and test generation. IEEE Trans. on Computers, 1998.","key":"36_CR26","DOI":"10.1109\/12.656068"},{"doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.","key":"36_CR27","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"36_CR28","volume-title":"The Complexity of Boolean Functions","author":"R. G. Nigmatulin","year":"1990","unstructured":"R. G. Nigmatulin. The Complexity of Boolean Functions. Nauka, Main Editorial Board for Phys. and Math. Lit., Moscow, 1990."},{"key":"36_CR29","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"Proc. 5th Int. Symp. on Progr.","author":"J.P. Queille","year":"1981","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th Int. Symp. on Progr., LNCS 137, pp. 337\u2013351. Springer-Verlag, 1981."},{"doi-asserted-by":"crossref","unstructured":"I. Wegener. The Complexity of Boolean Functions. JohnWiley & Sons, 1987.","key":"36_CR30","DOI":"10.1007\/3-540-18170-9_185"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45319-9_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T10:27:35Z","timestamp":1683973655000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45319-9_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418658","9783540453192"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-45319-9_36","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}