{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T06:45:15Z","timestamp":1750747515547},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540423454"},{"type":"electronic","value":"9783540445852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44585-4_7","type":"book-chapter","created":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T19:39:50Z","timestamp":1265917190000},"page":"66-78","source":"Crossref","is-referenced-by-count":38,"title":["A Practical Approach to Coverage in Model Checking"],"prefix":"10.1007","author":[{"given":"Hana","family":"Chockler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert P.","family":"Kurshan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"7_CR1","series-title":"Lect Notes Comput Sci","first-page":"62","volume-title":"Temporal Logic in Specification","author":"B. Banieqbal","year":"1987","unstructured":"B. Banieqbal and H. Barringer. Temporal logic with fixed points. In Temporal Logic in Specification, LNCS 398, pp. 62\u201374, 1987."},{"key":"7_CR2","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.","DOI":"10.1145\/196244.196575"},{"key":"7_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/3-540-63166-6_28","volume-title":"Efficient detection of vacuity in ACTL formulas","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":"7_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Efficient local model-checking for fragments of the modal \u00b5-calculus","author":"G. Bhat","year":"1996","unstructured":"G. Bhat and R. Cleaveland. Efficient local model-checking for fragments of the modal \u00b5-calculus. In Proc. TACAS, LNCS 1055, 1996."},{"key":"7_CR5","series-title":"Lect Notes Comput Sci","volume-title":"FMCAD","author":"R. Bloem","year":"2000","unstructured":"R. Bloem, H.N. Gabow, and F. Somenzi. An algorithm for strongly connected component analysis in n log n symbolic steps. In FMCAD, LNCS, 2000."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"J.P. Bergmann and M.A. Horowitz. Improving coverage analysis and test generation for large designs. In Proc 11th CAD, pp. 580\u2013584, November 1999.","DOI":"10.1109\/ICCAD.1999.810714"},{"key":"7_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/3-540-48683-6_21","volume-title":"Efficient decision procedures for model checking of linear time logic properties","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 Proc. 11th CAV, LNCS 1633, pp. 222\u2013235, 1999."},{"key":"7_CR8","unstructured":"J.R. B\u00fcchi. On a decision method in restricted second order arithmetic. In Proc. Internat. Congr. Logic, Method. and Philos. Sci. 1960, pp. 1\u201312, Stanford, 1962. Stanford University Press."},{"key":"7_CR9","series-title":"Lect Notes Comput Sci","first-page":"52","volume-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","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, 1981."},{"key":"7_CR10","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.","DOI":"10.1145\/217474.217565"},{"key":"7_CR11","unstructured":"E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"7_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1007\/3-540-45319-9_36","volume-title":"TACAS","author":"H. Chockler","year":"2001","unstructured":"H. Chockler, O. Kupferman, and M.Y. Vardi. Coverage metrics for temporal logic model checking. In TACAS, LNCS 2031, pp. 528\u2013542, 2001."},{"key":"7_CR13","series-title":"Lect Notes Comput Sci","first-page":"48","volume-title":"A linear-time model-checking algorithm for the alternation-free modal \u00b5-calculus","author":"R. Cleaveland","year":"1991","unstructured":"R. Cleaveland and B. Steffen. A linear-time model-checking algorithm for the alternation-free modal \u00b5-calculus. In Proc. 3rd CAD, LNCS 575, pp. 48\u201358, 1991."},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"S. Devadas, A. Ghosh, and K. Keutzer. An observability-based code coverage metric for functional simulation. In Proc. 8th CAD, pp. 418\u2013425, 1996.","DOI":"10.1109\/ICCAD.1996.569832"},{"key":"7_CR15","unstructured":"E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional \u00b5-calculus. In Proc. 1st LICS, pp. 267\u2013278, Cambridge, June 1986."},{"key":"7_CR16","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. of the 36th DAC, pp. 666\u2013671, June 1999.","DOI":"10.1145\/309847.310023"},{"key":"7_CR17","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. of the 35th DAC, pp. 152\u2013157, June 1998.","DOI":"10.1145\/277044.277078"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"R.C. Ho and M.A. Horowitz. Validation coverage analysis for complex digital designs. In Proc 8th CAD, pp. 146\u2013151, November 1996.","DOI":"10.1109\/ICCAD.1996.569537"},{"key":"7_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"COSPAN","author":"R.H. Hardin","year":"1996","unstructured":"R.H. Hardin, Z. Har'el, and R.P. Kurshan. COSPAN. In Proc. 8th CAV LNCS 1102, pp. 423\u2013427, 1996."},{"key":"7_CR20","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.","DOI":"10.1145\/309847.309936"},{"key":"7_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-64358-3","volume-title":"From pre-historic to post-modern symbolic model checking","author":"T.A. Henzinger","year":"1998","unstructured":"T.A. Henzinger, O. Kupferman, and S. Qadeer. From pre-historic to post-modern symbolic model checking. In Proc 10th CAV, LNCS 1427, 1998."},{"key":"7_CR22","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. of ICDD, pp. 532\u2013537, October 1995.","DOI":"10.1109\/ICCD.1995.528919"},{"key":"7_CR23","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, June 1995.","DOI":"10.1145\/223982.224450"},{"key":"7_CR24","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":"K.-S. Katz","year":"1999","unstructured":"[KGG99]-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, 1999."},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"M. Kantrowitz and L. Noack. I'm done simulating: Now what? verification coverage analysis and correctness checking of the DEC chip 21164 alpha microprocessor. In Proc. 33th DAC, pp. 325\u2013330, June 1996.","DOI":"10.1109\/DAC.1996.545595"},{"key":"7_CR26","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u00b5-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"7_CR27","unstructured":"O. Kupferman and A. Pnueli. Once and for all. In Proc. 10th IEEE Symp. on Logic in Comp. Sci., pp. 25\u201335, San Diego, June 1995."},{"key":"7_CR28","unstructured":"R.P. Kurshan. FormalCheck User\u2019s Manual. Cadence Design, Inc., 1998."},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi. Relating linear and branching model checking. In IFIP Work. Conf. on Programming Concepts and Methods, pp. 304\u2013326, New York, June 1998. Chapman & Hall.","DOI":"10.1007\/978-0-387-35358-6_21"},{"key":"7_CR30","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, 1999."},{"issue":"2","key":"7_CR31","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, March 2000.","journal-title":"Journal of the ACM"},{"key":"7_CR32","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.","DOI":"10.1145\/318593.318622"},{"key":"7_CR33","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.","DOI":"10.1109\/12.656068"},{"key":"7_CR34","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"Specification and verification of concurrent systems in Cesar","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 Programming, LNCS 137, pp. 337\u2013351, 1981."},{"key":"7_CR35","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A.P. Sistla","year":"1994","unstructured":"A.P. Sistla. Satefy, liveness and fairness in temporal logic. Formal Aspects of Computing, 6:495\u2013511, 1994.","journal-title":"Formal Aspects of Computing"},{"issue":"1","key":"7_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, November 1994.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44585-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T22:29:43Z","timestamp":1558823383000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44585-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423454","9783540445852"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-44585-4_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}