{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T09:30:39Z","timestamp":1744191039880,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026577"},{"type":"electronic","value":"9783642026584"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02658-4_11","type":"book-chapter","created":{"date-parts":[[2009,6,22]],"date-time":"2009-06-22T11:00:16Z","timestamp":1245668416000},"page":"94-108","source":"Crossref","is-referenced-by-count":40,"title":["Explaining Counterexamples Using Causality"],"prefix":"10.1007","author":[{"given":"Ilan","family":"Beer","sequence":"first","affiliation":[]},{"given":"Shoham","family":"Ben-David","sequence":"additional","affiliation":[]},{"given":"Hana","family":"Chockler","sequence":"additional","affiliation":[]},{"given":"Avigail","family":"Orni","sequence":"additional","affiliation":[]},{"given":"Richard","family":"Trefler","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"Prosyd: Property-Based System Design (2005), http:\/\/www.prosyd.org\/"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/3-540-36577-X_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2003","unstructured":"Armoni, R., Bustan, D., Kupferman, O., Vardi, M.Y.: Resets vs. aborts in linear temporal logic. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 65\u201380. Springer, Heidelberg (2003)"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Naik, M., Rajamani, S.: From symptom to cause: Localizing errors in counterexample traces. In: Proc. of POPL, pp. 97\u2013105 (2003)","DOI":"10.1145\/604131.604140"},{"key":"11_CR4","unstructured":"Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.: Explaining Counterexamples Using Causality. IBM technical report number H-0266, http:\/\/domino.watson.ibm.com\/library\/cyberdig.nsf\/Home"},{"issue":"2","key":"11_CR5","first-page":"101","volume":"22","author":"S. Ben-David","year":"2003","unstructured":"Ben-David, S., Eisner, C., Geist, D., Wolfsthal, Y.: Model checking at IBM. FMSD\u00a022(2), 101\u2013108 (2003)","journal-title":"FMSD"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-540-31984-9_17","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Chechik","year":"2005","unstructured":"Chechik, M., Gurfinkel, A.: A framework for counterexample generation and exploration. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol.\u00a03442, pp. 217\u2013233. Springer, Heidelberg (2005)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-78800-3_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Chockler","year":"2008","unstructured":"Chockler, H., Grumberg, O., Yadgar, A.: Efficient automatic STE refinement using responsibility. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 233\u2013248. Springer, Heidelberg (2008)"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Chockler, H., Halpern, J.Y., Kupferman, O.: What causes a system to satisfy a specification? ACM TOCL\u00a09(3) (2008)","DOI":"10.1145\/1352582.1352588"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E. Clarke","year":"1981","unstructured":"Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., McMillan, K., 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_CR11","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-44798-9_23","volume-title":"Correct Hardware Design and Verification Methods","author":"F. Copty","year":"2001","unstructured":"Copty, F., Irron, A., Weissberg, O., Kropp, N., Kamhi, G.: Efficient debugging in a formal verification environment. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 275\u2013292. Springer, Heidelberg (2001)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11814948_5","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"N. Dershowitz","year":"2006","unstructured":"Dershowitz, N., Hanna, Z., Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 36\u201341. Springer, Heidelberg (2006)"},{"key":"11_CR14","unstructured":"Dong, Y., Ramakrishnan, C.R., Smolka, S.A.: Model checking and evidence exploration. In: Proc. of ECBS, pp. 214\u2013223 (2003)"},{"key":"11_CR15","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Series on Integrated Circuits and Systems (2006)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-45069-6_3","volume-title":"Computer Aided Verification","author":"C. Eisner","year":"2003","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Campenhout, D.V.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 27\u201339. Springer, Heidelberg (2003)"},{"key":"11_CR17","unstructured":"Eiter, T., Lukasiewicz, T.: Complexity results for structure-based causality. In: Proc. 7th IJCAI, pp. 35\u201340 (2001)"},{"issue":"4","key":"11_CR18","first-page":"95","volume":"174","author":"A. Griesmayer","year":"2007","unstructured":"Griesmayer, A., Staber, S., Bloem, R.: Automated fault localization for c programs. ENTCS\u00a0174(4), 95\u2013111 (2007)","journal-title":"ENTCS"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-24730-2_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Groce","year":"2004","unstructured":"Groce, A.: Error explanation with distance metrics. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 108\u2013122. Springer, Heidelberg (2004)"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Groce, A., Kroening, D.: Making the most of BMC counterexamples. In: SGSH (July 2004)","DOI":"10.1016\/j.entcs.2004.12.023"},{"key":"11_CR21","series-title":"Causation and Counterfactuals","volume-title":"Two concepts of causation","author":"N. Hall","year":"2002","unstructured":"Hall, N.: Two concepts of causation. Causation and Counterfactuals. MIT Press, Cambridge (2002)"},{"key":"11_CR22","first-page":"194","volume-title":"Proc. of 17th UAI","author":"J. Halpern","year":"2001","unstructured":"Halpern, J., Pearl, J.: Causes and explanations: A structural-model approach \u2014 part I: Causes. In: Proc. of 17th UAI, pp. 194\u2013202. Morgan Kaufmann Publishers, San Francisco (2001)"},{"key":"11_CR23","volume-title":"A treatise of human nature","author":"D. Hume","year":"1939","unstructured":"Hume, D.: A treatise of human nature. John Noon, London (1939)"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/3-540-46002-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Jin","year":"2002","unstructured":"Jin, H., Ravi, K., Somenzi, F.: Fate and free will in error traces. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 445\u2013458. Springer, Heidelberg (2002)"},{"issue":"2","key":"11_CR25","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M., Wolper, P.: An automata-theoretic approach to branching-time model checking. JACM\u00a047(2), 312\u2013360 (2000)","journal-title":"JACM"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Maidl, M.: The common fragment of CTL and LTL. In: Proc. of FOCS, pp. 643\u2013652 (2000)","DOI":"10.1109\/SFCS.2000.892332"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J. Queille","year":"1981","unstructured":"Queille, J., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1981)"},{"key":"11_CR28","unstructured":"RuleBase\u00a0PE homepage, http:\/\/www.haifa.il.ibm.com\/projects\/verification\/RB_Homepage"},{"key":"11_CR29","unstructured":"Shen, S., Qin, Y., Li, S.: A faster counterexample minization algorithm based on refutation analysis. In: Proc. of DATE, pp. 672\u2013677 (2005)"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-72788-0_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"S. Staber","year":"2007","unstructured":"Staber, S., Bloem, R.: Fault localization and correction with QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 355\u2013368. Springer, Heidelberg (2007)"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"S\u00fclflow, A., Fey, G., Bloem, R., Drechsler, R.: Using unsatisfiable cores to debug multiple design errors. In: Proc. of Symp. on VLSI, pp. 77\u201382 (2008)","DOI":"10.1145\/1366110.1366131"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11901914_9","volume-title":"Automated Technology for Verification and Analysis","author":"C. Wang","year":"2006","unstructured":"Wang, C., Yang, Z., Ivancic, F., Gupta, A.: Whodunit? causal analysis for counterexamples. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 82\u201395. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02658-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T07:58:01Z","timestamp":1739174281000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02658-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026577","9783642026584"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02658-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}