{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:31Z","timestamp":1763468011666},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540203636"},{"type":"electronic","value":"9783540397243"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39724-3_11","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T21:15:55Z","timestamp":1294434955000},"page":"111-125","source":"Crossref","is-referenced-by-count":44,"title":["Coverage Metrics for Formal Verification"],"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","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-540-45069-6_35","volume-title":"Computer Aided Verification","author":"R. Armon","year":"2003","unstructured":"Armon, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Vardi, M.Y.: Enhanced vacuity detection for linear temporal logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 368\u2013380. Springer, Heidelberg (2003)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-46002-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 296\u2013311. Springer, Heidelberg (2002)"},{"key":"11_CR3","first-page":"596","volume-title":"Proc. 31st DAC","author":"D. Beatty","year":"1994","unstructured":"Beatty, D., Bryant, R.: Formally verifying a microprocessor using a simulation methodology. In: Proc. 31st DAC, pp. 596\u2013602. IEEE Computer Society, Los Alamitos (1994)"},{"issue":"2","key":"11_CR4","doi-asserted-by":"publisher","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 in System Design\u00a018(2), 141\u2013162 (2001)","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"11_CR5","first-page":"142","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. I&C\u00a098(2), 142\u2013170 (1992)","journal-title":"I&C"},{"key":"11_CR6","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 Academic Publishers, Dordrecht (2000)"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on java predicates. In: Proc. ISSTA, pp. 123\u2013133 (2002)","DOI":"10.1145\/566172.566191"},{"key":"11_CR8","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. ICLMP, pp. 1\u201312 (1962)"},{"key":"11_CR9","unstructured":"Budd, T.A.: Mutation analysis: Ideas, examples, problems, and prospects. Computer Program Testing, 129\u2013148 (1981)"},{"key":"11_CR10","unstructured":"Cadence. Assertion-based verification (2003), http:\/\/www.cadence.com"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proc. 32nd DAC, pp. 427\u2013432 (1995)","DOI":"10.1145\/217474.217565"},{"key":"11_CR12","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"11_CR13","unstructured":"Chockler, H.: Coverage metrics for model checking. PhD thesis, Hebrew University, Jerusalem, Israel (2003)"},{"key":"11_CR14","first-page":"409","volume-title":"Proc. 2nd TCS","author":"H. Chockler","year":"2002","unstructured":"Chockler, H., Kupferman, O.: Coverage of implementations by simulating specifications. In: Proc. 2nd TCS, vol.\u00a0223, pp. 409\u2013421. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-44585-4_7","volume-title":"Computer Aided Verification","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: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 66\u201378. Springer, Heidelberg (2001)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/3-540-45319-9_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage metrics for temporal logic model checking. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 528\u2013542. Springer, Heidelberg (2001)"},{"key":"11_CR17","first-page":"328","volume-title":"Proc. 35st DAC","author":"D.L. Dill","year":"1998","unstructured":"Dill, D.L.: What\u2019s between simulation and formal verification? In. In: Proc. 35st DAC, pp. 328\u2013329. IEEE Computer Society, Los Alamitos (1998)"},{"issue":"4","key":"11_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 Computer\u00a011(4), 34\u201343 (1978)","journal-title":"IEEE Computer"},{"key":"11_CR19","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: Proc. DAC, pp. 151\u2013156 (1995)","DOI":"10.1145\/217474.217522"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Ho, R.C., Horowitz, M.A.: Validation coverage analysis for complex digital designs. In: Proc. ICCAD, pp. 146\u2013151 (1996)","DOI":"10.1109\/ICCAD.1996.569537"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019el, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 423\u2013427. Springer, Heidelberg (1996)"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Hoskote, Y., Kam, T., Ho, P.-H., Zhao, X.: Coverage estimation for symbolic model checking. In: Proc. 36th DAC, pp. 300\u2013305 (1999)","DOI":"10.1145\/309847.309936"},{"issue":"5","key":"11_CR23","doi-asserted-by":"publisher","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. on Software Engineering\u00a023(5), 279\u2013295 (1997); Special issue on Formal Methods in Software Practice","journal-title":"IEEE Trans. on Software Engineering"},{"key":"11_CR24","unstructured":"Hoskote, Y.V.: Formal techniques for verification of synchronous sequential circuits. PhD thesis, The University of Texas at Austin (1995)"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/3-540-48153-2_21","volume-title":"Correct Hardware Design and Verification Methods","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: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 280\u2013297. Springer, Heidelberg (1999)"},{"key":"11_CR26","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: Proc. DAC, pp. 325\u2013330 (1996)","DOI":"10.1109\/DAC.1996.545595"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P.: Formal verification in a commercial setting. In: Proc. DAC 1997, vol.\u00a034, pp. 258\u2013262 (1997)","DOI":"10.1145\/266021.266089"},{"key":"11_CR28","unstructured":"Kurshan, R.P.: FormalCheck User\u2019s Manual. Cadence Design, Inc. (1998)"},{"issue":"2","key":"11_CR29","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O. Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. Journal on Software Tools For Technology Transfer\u00a04(2), 224\u2013233 (2003)","journal-title":"Journal on Software Tools For Technology Transfer"},{"key":"11_CR30","unstructured":"Marick, B.: How to misuse code coverage. In: Proc. 16th ICTCS (June 1999)"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification (1992)","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Peled, D.: Software Reliability Methods (2001)","DOI":"10.1007\/978-1-4757-3540-6"},{"key":"11_CR33","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/3-540-45657-0_39","volume-title":"Computer Aided Verification","author":"M. Purandare","year":"2002","unstructured":"Purandare, M., Somenzi, F.: Vacuum cleaning CTL formulae. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 485\u2013499. Springer, Heidelberg (2002)"},{"issue":"1-2","key":"11_CR34","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. Journal of Electronic Testing\u00a016(1-2), 67\u201381 (1999)","journal-title":"Journal of Electronic Testing"},{"issue":"4","key":"11_CR35","doi-asserted-by":"publisher","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 Design and Test of Computers\u00a018(4), 36\u201345 (2001)","journal-title":"IEEE Design and Test of Computers"},{"key":"11_CR36","unstructured":"Ur, S., Ziv, A.: Off-the-shelf vs. custom made coverage models, which is the one for you? In: Proc. ICSTAR (1998)"},{"key":"11_CR37","unstructured":"Verisity. Surecove\u2019s code coverage technology (2003), http:\/\/www.verisity.com\/products\/surecov.html"},{"key":"11_CR38","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st LICS, pp. 332\u2013344 (1986)"},{"issue":"1","key":"11_CR39","first-page":"1","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I&C\u00a0115(1), 1\u201337 (1994)","journal-title":"I&C"},{"issue":"4","key":"11_CR40","doi-asserted-by":"publisher","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 Computing Surveys\u00a029(4), 366\u2013427 (1997)","journal-title":"ACM Computing Surveys"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39724-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T14:03:28Z","timestamp":1559916208000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39724-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203636","9783540397243"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39724-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}