{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T10:40:29Z","timestamp":1736419229106,"version":"3.32.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2006,5,1]],"date-time":"2006-05-01T00:00:00Z","timestamp":1146441600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2006,5]]},"DOI":"10.1007\/s10703-006-0001-6","type":"journal-article","created":{"date-parts":[[2006,6,12]],"date-time":"2006-06-12T11:08:49Z","timestamp":1150110529000},"page":"189-212","source":"Crossref","is-referenced-by-count":19,"title":["Coverage metrics for temporal logic model checking*"],"prefix":"10.1007","volume":"28","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":[[2006,6,2]]},"reference":[{"unstructured":"R. Armoni, L. Fix, A. Flaisher, O. Grumberg, N. Piterman, A. Tiemeyer, and M.Y. Vardi, \u201cEnhanced vacuity detection in linear temporal logic,\u201d in Proceedings of 15th International Conference in Computer Aided Verification (CAV), vol. 2725 of Lecture Notes in Computer Science, Springer, 2003. pp. 368\u2013380.","key":"1_CR1"},{"doi-asserted-by":"crossref","unstructured":"D. Beaty and R. Bryant, \u201cFormally verifying a microprocessor using a simulation methodology,\u201d in Proc. 31st Design Automation Conference, IEEE Computer Society, 1994, pp. 596\u2013602.","key":"1_CR2","DOI":"10.1145\/196244.196575"},{"doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh, \u201cEfficient detection of vacuity in ACTL formulas,\u201d Form. Meth. in Sys. Des., Vol. 18, No. 2, pp. 141\u2013163, 2001.","key":"1_CR3","DOI":"10.1023\/A:1008779610539"},{"doi-asserted-by":"crossref","unstructured":"J.P. Bergmann and M.A. Horowitz, \u201cImproving coverage analysis and test generation for large designs,\u201d In IEEE International Conference for Computer-Aided Design, Nov. 1999, pp. 580\u2013584.","key":"1_CR4","DOI":"10.1109\/ICCAD.1999.810714"},{"doi-asserted-by":"crossref","unstructured":"D. Bustan, A. Flaisher, O. Grumberg, O. Kupferman, and M.Y. Vardi, \u201cRegular vacuity,\u201d in 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, volume 3725 of Lecture Notes in Computer Science, Springer-Verlag, 2005, pp. 191\u2013206.","key":"1_CR5","DOI":"10.1007\/11560548_16"},{"doi-asserted-by":"crossref","unstructured":"K.-T. Cheng and A. Krishnakumar, \u201cAutomatic functional test generation using the extended finite state machine model,\u201d in Proceedings of 30th Design Automation Conference, June 1993, pp. 86\u201391.","key":"1_CR6","DOI":"10.1145\/157485.164585"},{"doi-asserted-by":"crossref","unstructured":"H. Chockler, O. Kupferman, and M.Y. Vardi, \u201cCoverage metrics for formal verification. charme 2003: 111\u2013125,\u201d in Proceedings of 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), number 2860 in Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 111\u2013125.","key":"1_CR7","DOI":"10.1007\/978-3-540-39724-3_11"},{"doi-asserted-by":"crossref","unstructured":"E.M. Clarke and E.A. Emerson, \u201cDesign and synthesis of synchronization skeletons using branching time temporal logic,\u201d in Proc. Workshop on Logic of Programs, vol. 131 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 52\u201371.","key":"1_CR8","DOI":"10.1007\/BFb0025774"},{"doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long, \u201cModel checking and abstraction,\u201d in Proc. 19th ACM Symp. on Principles of Programming Languages, Albuquerque, New Mexico, Jan. 1992, pp. 343\u2013354.","key":"1_CR9","DOI":"10.1145\/143165.143235"},{"doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, K.L. McMillan, and X. Zhao, \u201cEfficient generation of counterexamples and witnesses in symbolic model checking,\u201d in Proc. 32nd Design Automation Conference, IEEE Computer Society, 1995, pp. 427\u2013432.","key":"1_CR10","DOI":"10.1109\/DAC.1995.249985"},{"unstructured":"E.M. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 1999.","key":"1_CR11"},{"doi-asserted-by":"crossref","unstructured":"S. Devadas, A. Ghosh, and K. Keutzer, \u201cAn observability-based code coverage metric for functional simulation,\u201d in Proceedings of the International Conference on Computer-Aided Design, Nov. 1996, pp. 418\u2013425.","key":"1_CR12","DOI":"10.1109\/ICCAD.1996.569832"},{"doi-asserted-by":"crossref","unstructured":"E.A. Emerson, \u201cTemporal and modal logic,\u201d Handbook of Theoretical Computer Science, 1990, pp. 997\u20131072.","key":"1_CR13","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"doi-asserted-by":"crossref","unstructured":"F. Fallah, P. Ashar, and S. Devadas, \u201cSimulation vector generation from hdl descriptions for observability enhanced-statement coverage,\u201d in Proceedings of the 36th Design Automation Conference, June 1999, pp. 666\u2013671.","key":"1_CR14","DOI":"10.1145\/309847.310023"},{"doi-asserted-by":"crossref","unstructured":"F. Fallah, S. Devadas, and K. Keutzer, \u201cOCCOM: Efficient computation of observability-based code coverage metrics for functional simulation,\u201c in Proceedings of the 35th Design Automation Conference, June 1998, pp. 152\u2013157.","key":"1_CR15","DOI":"10.1145\/277044.277078"},{"unstructured":"G.D. Hachtel and F. Somenzi, Logic Synthesis and Verification Algorithms. Kluwer Academic Publishers, Norwell, Massachusetts, 1996.","key":"1_CR16"},{"doi-asserted-by":"crossref","unstructured":"D. Harel and A. Pnueli, \u201cOn the development of reactive systems,\u201d in K. Apt (Ed.) Logics and Models of Concurrent Systems, vol. F-13 of NATO Advanced Summer Institutes, Springer-Verlag, 1985, pp. 477\u2013498.","key":"1_CR17","DOI":"10.1007\/978-3-642-82453-1_17"},{"unstructured":"R.C. Ho and M.A. Horowitz, \u201cValidation coverage analysis for complex digital designs,\u201d in International Conference on Computer Aided Design, Nov. 1996, pp. 146\u2013151.","key":"1_CR18"},{"doi-asserted-by":"crossref","unstructured":"R. Ho, C. Yang, M. Horowitz, and D. Dill, \u201cArchitecture validation for processors,\u201d in Proceedings of the 22nd Annual Symp. on Computer Architecture, June 1995, pp. 404\u2013413.","key":"1_CR19","DOI":"10.1145\/225830.224450"},{"doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare, Communicating Sequential Processes. Prentice-Hall, 1985.","key":"1_CR20","DOI":"10.1007\/978-3-642-82921-5_4"},{"doi-asserted-by":"crossref","unstructured":"Y. Hoskote, T. Kam, P.-H Ho, and X. Zhao, \u201cCoverage estimation for symbolic model checking,\u201d in Proc. 36th Design automation conference, 1999, pp. 300\u2013305.","key":"1_CR21","DOI":"10.1145\/309847.309936"},{"doi-asserted-by":"crossref","unstructured":"Y. Hoskote, D. Moundanos, and J. Abraham, \u201cAutomatic extraction of the control flow machine and application to evaluating coverage of verification vectors,\u201d in Proceedings of ICDD, Oct. 1995, pp. 532\u2013537.","key":"1_CR22","DOI":"10.1109\/ICCD.1995.528919"},{"doi-asserted-by":"crossref","unstructured":"N. Jayakumar, M. Purandare, and F. Somenzi, \u201cDos and don'ts of ctl state coverage estimation,\u201d in Proc. 40th Design Automation Conference (DAC), IEEE Computer Society, 2003.","key":"1_CR23","DOI":"10.1145\/775832.775908"},{"doi-asserted-by":"crossref","unstructured":"M. Kantrowitz and L. Noack, \u201cI'm done simulating: Now what? verification coverage analysis and correctness checking of the dec chip 21164 alpha microprocessor,\u201d in Proceedings of Design Automation Conference, June 1996, pp. 325\u2013330.","key":"1_CR24","DOI":"10.1145\/240518.240580"},{"doi-asserted-by":"crossref","unstructured":"S. Katz, D. Geist, and O. Grumberg, \u201cHave I written enough properties ?\u201d A method of comparison between specification and implementation,\u201d in 10th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science. Springer-Verlag, 1999.","key":"1_CR25","DOI":"10.1007\/3-540-48153-2_21"},{"doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi, \u201cVacuity detection in temporal model checking,\u201d International Journal on Software Tools for Technology Transfer (STTT), Vol. 4, No. 2, pp. 224\u2013233, 2003.","key":"1_CR26","DOI":"10.1007\/s100090100062"},{"doi-asserted-by":"crossref","unstructured":"O. Kupferman, M.Y. Vardi, and P. Wolper, \u201cAn automata-theoretic approach to branching-time model checking,\u201d J. ACM, Vol. 47, No. 2, pp. 312\u2013360, March 2000.","key":"1_CR27","DOI":"10.1145\/333979.333987"},{"unstructured":"R.P. Kurshan, FormalCheck User's Manual. Cadence Design, Inc., 1998.","key":"1_CR28"},{"doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli, \u201cChecking that finite state concurrent programs satisfy their linear specification,\u201d in Proc. 12th ACM Symp. on Principles of Programming Languages, New Orleans, Jan. 1985, pp. 97\u2013107.","key":"1_CR29","DOI":"10.1145\/318593.318622"},{"doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, Jan. 1992.","key":"1_CR30","DOI":"10.1007\/978-1-4612-0931-7"},{"doi-asserted-by":"crossref","unstructured":"D. Moumdanos, J.A. Abraham, and Y.V. Hoskote, \u201cAbstraction techniques for validation coverage analysis and test generation,\u201d IEEE Trans. Comp., Jan. 1998.","key":"1_CR31","DOI":"10.1109\/12.656068"},{"unstructured":"R.G. Nigmatulin, The Complexity of Boolean Functions. Nauka, Main Editorial Board for Physical and Mathematical Literature, Moscow, 1990.","key":"1_CR32"},{"doi-asserted-by":"crossref","unstructured":"M. Purandare and F. Somenzi, \u201cVacuum cleaning ctl formulae,\u201d in Proceedings of 14th International Conference in Computer Aided Verification (CAV), Lecture Notes in Computer Science, Springer, 2002. pp. 485\u2013499.","key":"1_CR33","DOI":"10.1007\/3-540-45657-0_39"},{"doi-asserted-by":"crossref","unstructured":"J.P. Queille and J. Sifakis, \u201cSpecification and verification of concurrent systems in Cesar,\u201d in Proc. 5th International Symp. on Programming, vol. 137 of Lecture Notes in Computer Science, Springer-Verlag, 1981. pp. 337\u2013351.","key":"1_CR34","DOI":"10.1007\/3-540-11494-7_22"},{"doi-asserted-by":"crossref","unstructured":"I. Wegener, The Complexity of Boolean Functions. John Wiley & Sons, Chichester, 1987.","key":"1_CR35","DOI":"10.1007\/3-540-18170-9_185"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0001-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0001-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0001-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T09:55:43Z","timestamp":1736416543000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0001-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,5]]},"references-count":35,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,5]]}},"alternative-id":["1"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0001-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2006,5]]}}}