{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,7]],"date-time":"2026-04-07T16:01:15Z","timestamp":1775577675021,"version":"3.50.1"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2008,6,1]],"date-time":"2008-06-01T00:00:00Z","timestamp":1212278400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000005","name":"U.S. Department of Defense","doi-asserted-by":"publisher","award":["N00014-01-1-0795N00014-04-1-0725"],"award-info":[{"award-number":["N00014-01-1-0795N00014-04-1-0725"]}],"id":[{"id":"10.13039\/100000005","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-05-1-0055"],"award-info":[{"award-number":["FA9550-05-1-0055"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000145","name":"Division of Information and Intelligent Systems","doi-asserted-by":"publisher","award":["CCR-0208535ITR-0325453IIS-0534064"],"award-info":[{"award-number":["CCR-0208535ITR-0325453IIS-0534064"]}],"id":[{"id":"10.13039\/100000145","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-0208535ITR-0325453IIS-0534064"],"award-info":[{"award-number":["CCR-0208535ITR-0325453IIS-0534064"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2008,6]]},"abstract":"<jats:p>Even when a system is proven to be correct with respect to a specification, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the system.<jats:italic>Coverage metrics<\/jats:italic>attempt to check which parts of a system are actually relevant for the verification process to succeed. Recent work on coverage in model checking suggests several coverage metrics and algorithms for finding parts of the system that are not covered by the specification. The work has already proven to be effective in practice, detecting design errors that escape early verification efforts in industrial settings. In this article, we relate a formal definition of causality given by Halpern and Pearl to coverage. We show that it gives significant insight into unresolved issues regarding the definition of coverage and leads to potentially useful extensions of coverage. In particular, we introduce the notion of<jats:italic>responsibility<\/jats:italic>, which assigns to components of a system a quantitative measure of their relevance to the satisfaction of the specification.<\/jats:p>","DOI":"10.1145\/1352582.1352588","type":"journal-article","created":{"date-parts":[[2008,6,10]],"date-time":"2008-06-10T13:30:05Z","timestamp":1213104605000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":49,"title":["What causes a system to satisfy a specification?"],"prefix":"10.1145","volume":"9","author":[{"given":"Hana","family":"Chockler","sequence":"first","affiliation":[{"name":"IBM Research, Haifa, Israel"}]},{"given":"Joseph Y.","family":"Halpern","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY"}]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[{"name":"Hebrew University, Jerusalem, Israel"}]}],"member":"320","published-online":{"date-parts":[[2008,6,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218539301000530"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/196244.196575"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 9th Conference on Computer Aided Verification. Lecture Notes in Computer Science.","volume":"1254","author":"Beer I."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008779610539"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the International Symposium on Software Reliability Engineering (ISSRE'96)","author":"Bieman J."},{"key":"e_1_2_1_6_1","unstructured":"Budd T. 1981. Mutation analysis: Ideas examples problems and prospects. In Computer Program Testing. B. Chandrasekaran and S. Radichi Eds. North-Holland Amsterdam The Netherlands 129--148.]] Budd T. 1981. Mutation analysis: Ideas examples problems and prospects. In Computer Program Testing. B. Chandrasekaran and S. Radichi Eds. North-Holland Amsterdam The Netherlands 129--148.]]"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625279"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622487.1622491"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Chockler H. and Kupferman O . 2002 . Coverage of implementations by simulating specifications. In Proceedings of 2nd IFIP International Conference on Theoretical Computer Science Volume 223 of IFIP Conference Proceedings (Montreal Canada) R. Baeza-Yates U. Montanari and N. Santoro Eds. Kluwer Academic Publishers Dordretch The Netherlands 409--421.]] Chockler H. and Kupferman O. 2002. Coverage of implementations by simulating specifications. In Proceedings of 2nd IFIP International Conference on Theoretical Computer Science Volume 223 of IFIP Conference Proceedings (Montreal Canada) R. Baeza-Yates U. Montanari and N. Santoro Eds. Kluwer Academic Publishers Dordretch The Netherlands 409--421.]]","DOI":"10.1007\/978-0-387-35608-2_34"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 13th International Conference. Lecture Notes in Computer Science","volume":"2102","author":"Chockler H."},{"key":"e_1_2_1_11_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science","volume":"2031","author":"Chockler H."},{"key":"e_1_2_1_12_1","volume-title":"Lecture Notes in Computer Science","volume":"2860","author":"Chockler H."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/217474.217565"},{"key":"e_1_2_1_14_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press Cambridge MA.]] Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press Cambridge MA.]]"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/C-M.1978.218136"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277138"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 18th Conference on Uncertainty in Artificial Intelligence (UAI","author":"Eiter T.","year":"2002"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00271-0"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"e_1_2_1_20_1","unstructured":"Groce A. Chaki S. Kroening D. and Strichman O. 2008. Error explanation with distance metrics. Int. J. Softw. Tools Tech. Transf. (STTT). To appear.]] Groce A. Chaki S. Kroening D. and Strichman O. 2008. Error explanation with distance metrics. Int. J. Softw. Tools Tech. Transf. (STTT). To appear.]]"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Hall N. 2004. Two concepts of causation. In Causation and Counterfactuals. J. Collins N. Hall and L. A. Paul Eds. MIT Press Cambridge MA.]] Hall N. 2004. Two concepts of causation. In Causation and Counterfactuals. J. Collins N. Hall and L. A. Paul Eds. MIT Press Cambridge MA.]]","DOI":"10.7551\/mitpress\/1752.003.0010"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1093\/bjps\/axi147"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309936"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Hume D. 1739. A Treatise of Human Nature. John Noon London U.K.]] Hume D. 1739. A Treatise of Human Nature. John Noon London U.K.]]","DOI":"10.1093\/oseo\/instance.00046221"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775908"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(88)90039-6"},{"key":"e_1_2_1_27_1","volume-title":"10th Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science","volume":"1703","author":"Kupferman O."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100062"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"e_1_2_1_30_1","unstructured":"Kurshan R. 1998. FormalCheck User's Manual. Cadence Design Inc. San Jose CA.]] Kurshan R. 1998. FormalCheck User's Manual. Cadence Design Inc. San Jose CA.]]"},{"key":"e_1_2_1_31_1","unstructured":"Lynch N. 1996. Distributed Algorithms. Morgan Kaufmann San Francisco CA.]] Lynch N. 1996. Distributed Algorithms. Morgan Kaufmann San Francisco CA.]]"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/C-M.1978.218136"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.92910"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/62.322435"},{"key":"e_1_2_1_35_1","unstructured":"Papadimitriou C. H. 1994. Computational Complexity 2nd ed. Addison-Wesley Reading MA.]] Papadimitriou C. H. 1994. Computational Complexity 2nd ed. Addison-Wesley Reading MA.]]"},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Peled D. 2001. Software Reliability Methods. Springer-Verlag Berlin Germany.]] Peled D. 2001. Software Reliability Methods. Springer-Verlag Berlin Germany.]]","DOI":"10.1007\/978-1-4757-3540-6"},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Purandare M. and Somenzi F . 2002 . Vacuum cleaning CTL formulae. In Proceedings of the 14th Conference on Computer Aided Verification Lecture Notes in Computer Science vol. 2404 . Springer-Verlag Berlin Germany 485--499.]] Purandare M. and Somenzi F. 2002. Vacuum cleaning CTL formulae. In Proceedings of the 14th Conference on Computer Aided Verification Lecture Notes in Computer Science vol. 2404. Springer-Verlag Berlin Germany 485--499.]]","DOI":"10.1007\/3-540-45657-0_39"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/267580.267590"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1352582.1352588","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1352582.1352588","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:39:20Z","timestamp":1750253960000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1352582.1352588"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,6]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,6]]}},"alternative-id":["10.1145\/1352582.1352588"],"URL":"https:\/\/doi.org\/10.1145\/1352582.1352588","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,6]]},"assertion":[{"value":"2004-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2006-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-06-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}