{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T03:54:29Z","timestamp":1772078069111,"version":"3.50.1"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"4-5","license":[{"start":{"date-parts":[[2006,4,7]],"date-time":"2006-04-07T00:00:00Z","timestamp":1144368000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2006,8]]},"DOI":"10.1007\/s10009-004-0175-4","type":"journal-article","created":{"date-parts":[[2006,4,9]],"date-time":"2006-04-09T02:44:07Z","timestamp":1144550647000},"page":"373-386","source":"Crossref","is-referenced-by-count":23,"title":["Coverage metrics for formal verification"],"prefix":"10.1007","volume":"8","author":[{"given":"Hana","family":"Chockler","sequence":"first","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]},{"given":"Moshe","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,4,7]]},"reference":[{"key":"175_CR1","volume-title":"Proceedings of the 15th International Conference on Computer-Aided Verification","author":"R. Armoni","year":"2003","unstructured":"Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Vardi, M.Y.: Enhanced vacuity detection for linear temporal logic. In: Proceedings of the 15th International Conference on Computer-Aided Verification. Berlin, Heidelberg, New York: Springer 2003"},{"key":"175_CR2","first-page":"296","volume-title":"Lecture Notes in Computer Science","author":"R. Armoni","year":"2002","unstructured":"Armoni, R., Fix, L., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Tiemeyer, A., Singerman, E., Vardi, M.Y., Zbar, Y.: The ForSpec temporal language: a new temporal property-specification language. In: Procedings of the 8th Internationl Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201902). Lecture Notes in Computer Science, vol. 2280, pp. 296\u2013311. Berlin, Heidelberg, New York: Springer 2002"},{"key":"175_CR3","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/196244.196575","volume-title":"Proceedings of the 31st Design Automation Conference","author":"D. Beatty","year":"1994","unstructured":"Beatty, D., Bryant, R.: Formally verifying a microprocessor using a simulation methodology. In: Proceedings of the 31st Design Automation Conference, pp. 596\u2013602. IEEE Press, New York 1994"},{"issue":"2","key":"175_CR4","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. Formal Methods Syst. Des. 18(2), 141\u2013162 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"175_CR5","volume-title":"Principles of Verifiable RTL Design\u2013-a Functional Coding Style Supporting Verification Processes","author":"L. Bening","year":"2000","unstructured":"Bening, L., Foster, H.: Principles of Verifiable RTL Design \u2013 a Functional Coding Style Supporting Verification Processes. Kluwer, Dordrecht 2000"},{"key":"175_CR6","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on java predicates. In: Proceedings of ACM\/SIGSOFT International Symposium on Software Testing and Analysys (ISSTA), pp. 123\u2013133. Rome, Italy (2002)","DOI":"10.1145\/566172.566191"},{"issue":"2","key":"175_CR7","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142\u2013170(1992)","journal-title":"Inf. Comput."},{"key":"175_CR8","first-page":"1","volume-title":"Proceedings of the International Congress on Logic, Methods and Philosophical Science 1960","author":"J.R. B\u00fcchi","year":"1962","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of the International Congress on Logic, Methods and Philosophical Science 1960, pp. 1\u201312. Stanford: Stanford University Press 1962"},{"key":"175_CR9","unstructured":"Budd, T.A.: Mutation analysis: ideas, examples, problems, and prospects. In: Proceedings of the Conference on Software Testing, North Holland (1981)"},{"key":"175_CR10","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/BF00625279","volume":"18","author":"T.A. Budd","year":"1982","unstructured":"Budd, T.A., Angluin, D.: Two notions of correctness and their relation to testing. Acta Inf 18, 31\u201345 (1982)","journal-title":"Acta Inf"},{"key":"175_CR11","unstructured":"Cadence. Assertion-based verification. http:\/\/www.cadence.com (2003)"},{"key":"175_CR12","volume-title":"Coverage Metrics for Model Checking","author":"H. Chockler","year":"2003","unstructured":"Chockler, H.: Coverage Metrics for Model Checking. Ph.D. thesis, Hebrew University, Jerusalem, Israel (2003)"},{"key":"175_CR13","first-page":"409","volume-title":"Proceedings of the 2nd IFIP International Conference on Theoretical Computer Science, Proceedings of the IFIP Conference, Montreal","author":"H. Chockler","year":"2002","unstructured":"Chockler, H., Kupferman, O.: Coverage of implementations by simulating specifications. In: Baeza-Yates, R.A., Montanari, U., Santoro, N. (eds.): Proceedings of the 2nd IFIP International Conference on Theoretical Computer Science, Proceedings of the IFIP Conference, Montreal, vol. 223, pp. 409\u2013421. Kluwer, Dordrecht 2002"},{"key":"175_CR14","first-page":"66","volume-title":"Lecture Notes in Computer Science","author":"H. Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Kurshan, R.P., Vardi, M.Y.: A practical approach to coverage in model checking. In: Proceedings of the 13th International Conference on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 2102, pp. 66\u201378. Berlin, Heidelberg, New York: Springer 2001"},{"key":"175_CR15","first-page":"528","volume-title":"Lecture Notes in Computer Science","author":"H. Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage metrics for temporal logic model checking. In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2031, pp. 528\u2013542. Berlin, Heidelberg, New York: Springer 2001"},{"key":"175_CR16","first-page":"427","volume-title":"Proceedings of the 32nd Conference on Design Automation","author":"E.M. Clarke","year":"1995","unstructured":"Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proceedings of the 32nd Conference on Design Automation, pp. 427\u2013432. IEEE Press, New York 1995"},{"key":"175_CR17","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge, MA 1999"},{"issue":"4","key":"175_CR18","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1109\/C-M.1978.218136","volume":"11","author":"R.A. DeMillo","year":"1978","unstructured":"DeMillo, R.A., Lipton, R.J., Sayward, F.G.: Hints on test data selection: help for the practicing programmer. IEEE Comput. 11(4), 34\u201343 (1978)","journal-title":"IEEE Comput"},{"key":"175_CR19","first-page":"328","volume-title":"Proceedings of the 35st Conference on Design Automation","author":"D.L. Dill","year":"1998","unstructured":"Dill, D.L.: What\u2019s between simulation and formal verification? In: Proceedings of the 35st Conference on Design Automation, pp. 328\u2013329. IEEE Press, New York 1998"},{"key":"175_CR20","doi-asserted-by":"crossref","unstructured":"French, R.S., Lam, M.S., Levitt, J.R., Olukotun, K.: A general method for compiling event-driven simulations. In: Proceedings of the Conference on Design Automation, pp. 151\u2013156 (1995)","DOI":"10.1145\/217474.217522"},{"issue":"3","key":"175_CR21","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Programm. Lang. Syst. 16(3), 843\u2013871 (1994)","journal-title":"ACM Trans. Programm. Lang. Syst."},{"key":"175_CR22","first-page":"423","volume-title":"Lecture Notes in Computer Science","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019el, Z., Kurshan, R.P.: COSPAN. In: Proceedings of the 8th International Conference on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1102, pp. 423\u2013427. Berlin, Heidelberg, New York: Springer 1996"},{"key":"175_CR23","doi-asserted-by":"crossref","unstructured":"Ho, R.C., Horowitz, M.A.: Validation coverage analysis for complex digital designs. In: Proceedings of the International Conference on Computer-Aided Design, pp. 146\u2013151 (1996)","DOI":"10.1109\/ICCAD.1996.569537"},{"key":"175_CR24","unstructured":"Hoskote, Y.V.: Formal techniques for verification of synchronous sequential circuits. Ph.D. thesis, University of Texas at Austin (1995)"},{"issue":"5","key":"175_CR25","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"175_CR26","doi-asserted-by":"crossref","unstructured":"Hoskote, Y., Kam, T., Ho, P.-H., Zhao, X.: Coverage estimation for symbolic model checking. In: Proceedings of the 36th Conference on Design Automation, pp. 300\u2013305 (1999)","DOI":"10.1145\/309847.309936"},{"key":"175_CR27","doi-asserted-by":"crossref","unstructured":"Kantrowitz, M., Noack, L.: I\u2019m done simulating: now what? verification coverage analysis and correctness checking of the dec chip 21164 alpha microprocessor. In: Proceedings of the Conference on Design Automation, pp. 325\u2013330 (1996)","DOI":"10.1109\/DAC.1996.545595"},{"key":"175_CR28","unstructured":"Katz, S.: Techniques for increasing coverage of formal verification. M.Sc. thesis, The Technion, Israel (2001)"},{"key":"175_CR29","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/3-540-48153-2_21","volume-title":"Proceedings of the 10th Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science","author":"S. Katz","year":"1999","unstructured":"Katz, S., Geist, D., Grumberg, O.: \u201cHave I written enough properties ?\u201d a method of comparison between specification and implementation. In: Proceedings of the 10th Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science, vol. 1703, pp. 280\u2013297. Berlin, Heidelberg, New York: Springer 1999"},{"issue":"2","key":"175_CR30","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O. Kupferman","year":"2003","unstructured":"Kupferman, O., Vardim, M.Y.: Vacuity detection in temporal model checking. J. Softw. Tools Technol. Transfer 4(2), 224\u2013233 (2003)","journal-title":"J. Softw. Tools Technol. Transfer"},{"key":"175_CR31","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P.: Formal verification in a commercial setting. In: Proceedings of the Conference on Design Automation, vol. 34, pp. 258\u2013262 (1997)","DOI":"10.1109\/DAC.1997.597154"},{"key":"175_CR32","volume-title":"FormalCheck User\u2019s Manual","author":"R.P. Kurshan","year":"1998","unstructured":"Kurshan, R.P.: FormalCheck User\u2019s Manual. San Jose: Cadence Design 1998"},{"key":"175_CR33","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A: The Temporal Logic of Reactive and Concurrent Systems: Specification. Berlin, Heidelberg, New York: Springer 1992"},{"key":"175_CR34","unstructured":"Marick, B.: How to misuse code coverage. In: Proceedings of the 16th International Conference on Testing Computer Software (1999)"},{"key":"175_CR35","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3540-6","volume-title":"Software Reliability Methods","author":"D. Peled","year":"2001","unstructured":"Peled, D.: Software Reliability Methods. Berlin, Heidelberg, New York: Springer 2001"},{"key":"175_CR36","first-page":"485","volume-title":"Proceedings of the 14th Conference on Computer-Aided Verification. Lecture Notes in Computer Science","author":"M. Purandare","year":"2002","unstructured":"Purandare, M., Somenzi, F.: Vacuum cleaning CTL formulae. In: Proceedings of the 14th Conference on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 2404, pp. 485\u2013499. Berlin, Heidelberg, New York: Springer 2002"},{"issue":"1\u20132","key":"175_CR37","first-page":"67","volume":"16","author":"J. Shen","year":"1999","unstructured":"Shen, J., Abraham, J.A.: An rtl abstraction technique for processor microarchitecture validation and test generation. J. Electron. Test. 16(1\u20132), 67\u201381 (1999)","journal-title":"J. Electron. Test."},{"issue":"4","key":"175_CR38","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1109\/54.936247","volume":"18","author":"S. Tasiran","year":"2001","unstructured":"Tasiran, S., Keutzer, K.: Coverage metrics for functional validation of hardware designs. IEEE Des. Test Comput. 18(4), 36\u201345 (2001)","journal-title":"IEEE Des. Test Comput."},{"key":"175_CR39","unstructured":"Ur, S., Ziv., A.: Off-the-shelf vs. custom made coverage models, which is the one for you? In: Proceedings of the International Conference on Software Testing, Analysis, and Review (1998)"},{"key":"175_CR40","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st Symposium on Logic in Computer Science, pp. 332\u2013344. Cambridge, MA (1986)"},{"issue":"1","key":"175_CR41","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"175_CR42","unstructured":"Verisity. Surecove\u2019s code coverage technology. http:\/\/www.verisity.com\/products\/surecov.html (2003)"},{"issue":"4","key":"175_CR43","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1145\/267580.267590","volume":"29","author":"H. Zhu","year":"1997","unstructured":"Zhu, H., Hall, P.V., May, J.R.: Software unit test coverage and adequacy. ACM Comput. Surv. 29(4), 366\u2013427 (1997)","journal-title":"ACM Comput. Surv."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0175-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-004-0175-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0175-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:20Z","timestamp":1559100320000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-004-0175-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,4,7]]},"references-count":43,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2006,8]]}},"alternative-id":["175"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0175-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,4,7]]}}}