{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T03:37:39Z","timestamp":1777606659988,"version":"3.51.4"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2011,12,20]],"date-time":"2011-12-20T00:00:00Z","timestamp":1324339200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2012,2]]},"DOI":"10.1007\/s10703-011-0132-2","type":"journal-article","created":{"date-parts":[[2011,12,19]],"date-time":"2011-12-19T10:31:24Z","timestamp":1324290684000},"page":"20-40","source":"Crossref","is-referenced-by-count":72,"title":["Explaining counterexamples using causality"],"prefix":"10.1007","volume":"40","author":[{"given":"Ilan","family":"Beer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shoham","family":"Ben-David","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hana","family":"Chockler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Avigail","family":"Orni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Trefler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,12,20]]},"reference":[{"key":"132_CR1","unstructured":"Prosyd: Property-based system design (2005). http:\/\/www.prosyd.org\/"},{"key":"132_CR2","first-page":"97","volume-title":"Principles of programming languages","author":"T Ball","year":"2003","unstructured":"Ball T, Naik M, Rajamani S (2003) From symptom to cause: Localizing errors in counterexample traces. In: Principles of programming languages, pp 97\u2013105"},{"issue":"2","key":"132_CR3","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1023\/A:1022905120346","volume":"22","author":"S Ben-David","year":"2003","unstructured":"Ben-David S, Eisner C, Geist D, Wolfsthal Y (2003) Model checking at IBM. Form Methods Syst Des 22(2):101\u2013108","journal-title":"Form Methods Syst Des"},{"key":"132_CR4","first-page":"217","volume-title":"Proceedings of FASE\u201905","author":"M Chechik","year":"2005","unstructured":"Chechik M, Gurfinkel A (2005) A framework for counterexample generation and exploration. In: Proceedings of FASE\u201905, pp 217\u2013233"},{"key":"132_CR5","first-page":"233","volume-title":"TACAS","author":"H Chockler","year":"2008","unstructured":"Chockler H, Grumberg O, Yadgar A (2008) Efficient automatic STE refinement using responsibility. In: TACAS, pp 233\u2013248"},{"key":"132_CR6","doi-asserted-by":"crossref","unstructured":"Chockler H, Halpern JY, Kupferman O (2008) What causes a system to satisfy a specification? ACM Trans Comput Log 9(3)","DOI":"10.1145\/1352582.1352588"},{"key":"132_CR7","series-title":"Lecture notes in computer science","first-page":"52","volume-title":"Proc workshop on logic of programs","author":"E Clarke","year":"1981","unstructured":"Clarke E, Emerson E (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc workshop on logic of programs, Lecture notes in computer science, vol\u00a0131. Springer, Berlin, pp\u00a052\u201371"},{"key":"132_CR8","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1109\/DAC.1995.249985","volume-title":"Proc 32nd design automation conference","author":"E Clarke","year":"1995","unstructured":"Clarke E, Grumberg O, McMillan K, Zhao X (1995) Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proc 32nd design automation conference. IEEE Comput Soc, Los Alamitos, pp\u00a0427\u2013432"},{"key":"132_CR9","first-page":"275","volume-title":"Proceedings of CHARME\u201901","author":"F Copty","year":"2001","unstructured":"Copty F, Irron A, Weissberg O, Kropp N, Kamhi G (2001) Efficient debugging in a formal verification environment. In: Proceedings of CHARME\u201901, pp 275\u2013292"},{"key":"132_CR10","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/11814948_5","volume-title":"Proceedings of 9th international conference on theory and applications of satisfiability testing (SAT)","author":"N Dershowitz","year":"2006","unstructured":"Dershowitz N, Hanna Z, Nadel A (2006) A scalable algorithm for minimal unsatisfiable core extraction. In: Proceedings of 9th international conference on theory and applications of satisfiability testing (SAT), pp 36\u201341"},{"key":"132_CR11","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1109\/ECBS.2003.1194802","volume-title":"IEEE conference and workshops on engineering computer based systems","author":"Y Dong","year":"2003","unstructured":"Dong Y, Ramakrishnan CR, Smolka SA (2003) Model checking and evidence exploration. In: IEEE conference and workshops on engineering computer based systems, IEEE, Huntsville, pp 214\u2013223"},{"key":"132_CR12","series-title":"Series on integrated circuits and systems","volume-title":"A practical introduction to PSL","author":"C Eisner","year":"2006","unstructured":"Eisner C, Fisman D (2006) A practical introduction to PSL. Series on integrated circuits and systems. Springer, Berlin"},{"key":"132_CR13","series-title":"Lect notes in comp sci","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/978-3-540-45069-6_3","volume-title":"Proc 15th intl conference on computer aided verification (CAV\u201903)","author":"C Eisner","year":"2003","unstructured":"Eisner C, Fisman D, Havlicek J, Lustig Y, McIsaac A, Campenhout DV (2003) Reasoning with temporal logic on truncated paths. In: Proc 15th intl conference on computer aided verification (CAV\u201903). Lect notes in comp sci, vol\u00a02725. Springer, Boulder, pp\u00a027\u201339"},{"key":"132_CR14","first-page":"35","volume-title":"Proc 7th international joint conference on artificial intelligence","author":"T Eiter","year":"2001","unstructured":"Eiter T, Lukasiewicz T (2001) Complexity results for structure-based causality. In: Proc 7th international joint conference on artificial intelligence, pp 35\u201340"},{"key":"132_CR15","volume-title":"Uncertainty in artificial intelligence: proceedings of the 18th conference (UAI-2002)","author":"T Eiter","year":"2002","unstructured":"Eiter T, Lukasiewicz T (2002) Causes and explanations in the structural-model approach: Tractable cases. In: Uncertainty in artificial intelligence: proceedings of the 18th conference (UAI-2002). Morgan Kaufmann, Edmonton"},{"issue":"4","key":"132_CR16","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/j.entcs.2006.12.032","volume":"174","author":"A Griesmayer","year":"2007","unstructured":"Griesmayer A, Staber S, Bloem R (2007) Automated fault localization for C programs. Electron Notes Theor Comput Sci 174(4):95\u2013111","journal-title":"Electron Notes Theor Comput Sci"},{"key":"132_CR17","volume-title":"TACAS","author":"A Groce","year":"2004","unstructured":"Groce A (2004) Error explanation with distance metrics. In: TACAS"},{"issue":"3","key":"132_CR18","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/s10009-005-0202-0","volume":"8","author":"A Groce","year":"2006","unstructured":"Groce A, Chaki S, Kroening D, Strichman O (2006) Error explanation with distance metrics. STTT 8(3):229\u2013247","journal-title":"STTT"},{"key":"132_CR19","volume-title":"SGSH","author":"A Groce","year":"2004","unstructured":"Groce A, Kroening D (2004) Making the most of BMC counterexamples. In: SGSH"},{"key":"132_CR20","volume-title":"Causation and counterfactuals","author":"N Hall","year":"2002","unstructured":"Hall N (2002) Two concepts of causation. In: Collins J, Hall N, Paul LA (eds) Causation and counterfactuals. MIT Press, Cambridge"},{"key":"132_CR21","first-page":"194","volume-title":"Uncertainty in artificial intelligence: proceedings of the seventeenth conference (UAI-2001)","author":"J Halpern","year":"2001","unstructured":"Halpern J, Pearl J (2001) Causes and explanations: a structural-model approach\u2014part 1: Causes. In: Uncertainty in artificial intelligence: proceedings of the seventeenth conference (UAI-2001). Morgan Kaufmann, San Francisco, pp 194\u2013202"},{"key":"132_CR22","doi-asserted-by":"crossref","unstructured":"Halpern J, Pearl J (2005) Causes and explanations: a structural-model approach\u2014part 1: Causes. Br J Philos Sci 56:843\u2013887","DOI":"10.1093\/bjps\/axi147"},{"key":"132_CR23","volume-title":"A treatise of human nature","author":"D Hume","year":"1939","unstructured":"Hume D (1939) A treatise of human nature. John Noon, London"},{"key":"132_CR24","first-page":"445","volume-title":"TACAS02","author":"H Jin","year":"2002","unstructured":"Jin H, Ravi K, Somenzi F (2002) Fate and free will in error traces. In: TACAS02, pp 445\u2013458"},{"issue":"2","key":"132_CR25","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O Kupferman","year":"2000","unstructured":"Kupferman O, Vardi M, Wolper P (2000) An automata-theoretic approach to branching-time model checking. J ACM 47(2):312\u2013360","journal-title":"J ACM"},{"key":"132_CR26","volume-title":"The temporal logic of reactive and concurrent systems: safety","author":"Z Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) The temporal logic of reactive and concurrent systems: safety. Springer, New York"},{"key":"132_CR27","first-page":"46","volume-title":"18th IEEE symposium on foundation of computer science","author":"A Pnueli","year":"1977","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th IEEE symposium on foundation of computer science, pp 46\u201357"},{"key":"132_CR28","volume-title":"5th international symposium on programming","author":"J Quielle","year":"1982","unstructured":"Quielle J, Sifakis J (1982) Specification and verification of concurrent systems in CESAR. In: 5th international symposium on programming"},{"key":"132_CR29","unstructured":"RuleBase PE Homepage. http:\/\/www.haifa.il.ibm.com\/projects\/verification\/RB_Homepage"},{"key":"132_CR30","first-page":"672","volume-title":"DATE05","author":"S Shen","year":"2005","unstructured":"Shen S, Qin Y, Li S (2005) A faster counterexample minimization algorithm based on refutation analysis. In: DATE05, pp 672\u2013677"},{"key":"132_CR31","first-page":"355","volume-title":"SAT","author":"S Staber","year":"2007","unstructured":"Staber S, Bloem R (2007) Fault localization and correction with QBF. In: SAT, pp 355\u2013368"},{"key":"132_CR32","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1145\/1366110.1366131","volume-title":"ACM great lakes symposium on VLSI","author":"A S\u00fclflow","year":"2008","unstructured":"S\u00fclflow A, Fey G, Bloem R, Drechsler R (2008) Using unsatisfiable cores to debug multiple design errors. In: ACM great lakes symposium on VLSI, pp 77\u201382"},{"key":"132_CR33","first-page":"82","volume-title":"ATVA","author":"C Wang","year":"2006","unstructured":"Wang C, Yang Z, Ivancic F, Gupta A (2006) Whodunit? Causal analysis for counterexamples. In: ATVA, pp 82\u201395"},{"key":"132_CR34","first-page":"119","volume":"110\u2013111","author":"P Wolper","year":"1985","unstructured":"Wolper P (1985) The tableau method for temporal logic: an overview. Log Anal 110\u2013111:119\u2013136","journal-title":"Log Anal"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0132-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0132-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0132-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,21]],"date-time":"2021-12-21T00:21:09Z","timestamp":1640046069000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0132-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12,20]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,2]]}},"alternative-id":["132"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0132-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12,20]]}}}