{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,14]],"date-time":"2025-04-14T18:03:45Z","timestamp":1744653825813},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540472377"},{"type":"electronic","value":"9783540472384"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901914_9","type":"book-chapter","created":{"date-parts":[[2006,10,10]],"date-time":"2006-10-10T01:21:43Z","timestamp":1160443303000},"page":"82-95","source":"Crossref","is-referenced-by-count":28,"title":["Whodunit? Causal Analysis for Counterexamples"],"prefix":"10.1007","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[]},{"given":"Zijiang","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Franjo","family":"Ivan\u010di\u0107","sequence":"additional","affiliation":[]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"6","key":"9_CR1","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1002\/spe.4380230603","volume":"23","author":"H. Agrawal","year":"1993","unstructured":"Agrawal, H., DeMillo, R.A., Spafford, E.H.: Debugging with dynamic slicing and backtracking. Software - Practice and Experience\u00a023(6), 589\u2013616 (1993)","journal-title":"Software - Practice and Experience"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Sierawski, B.D., Sakallah, K.A.: Satometer: How much have we searched? In: Proceedings of the Design Automation Conference, New Orleans, LA, June 2002, pp. 737\u2013742 (2002)","DOI":"10.1145\/513918.514103"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: Localizing errors in counterexample traces. In: Symposium on Principles of Programming Languages (POPL 2003), January 2003, pp. 97\u2013105 (2003)","DOI":"10.1145\/604131.604140"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/3-540-63166-6_28","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1997","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 279\u2013290. Springer, Heidelberg (1997)"},{"key":"9_CR5","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.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: 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 (1982)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Cleve, H., Zeller, A.: Locating causes of program failures. In: ACM\/IEEE International Conference on Software Engineering (2005)","DOI":"10.1145\/1062455.1062522"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Coen-Porisini, A., Denaro, G., Ghezzi, C., Pezze, M.: Using symbolic execution for verifying safety-critical systems. In: European Software Engineering Conference\/Foundations of Software Engineering, pp. 142\u2013151 (2001)","DOI":"10.1145\/503209.503230"},{"key":"9_CR8","volume-title":"A Discipline of Programming","author":"E. Dijkstra","year":"1976","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_33","volume-title":"Computer Aided Verification","author":"A. Griesmayer","year":"2006","unstructured":"Griesmayer, A., Bloem, R., Cook, B.: Repair of boolean programs with an application to c. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, Springer, Heidelberg (2006)"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Groce, A., Chaki, S., Kroening, D., Strichman, O.: Error explanation with distance metrics. International Journal on Software Tools for Technology Transfer (2005)","DOI":"10.1007\/s10009-005-0202-0"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-44829-2_8","volume-title":"Model Checking Software","author":"A. Groce","year":"2003","unstructured":"Groce, A., Visser, W.: What went wrong: Explaining counterexamples. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 121\u2013135. Springer, Heidelberg (2003)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/3-540-48166-4_19","volume-title":"Software Engineering - ESEC\/FSE \u201999","author":"T. Gyim\u00f3thy","year":"1999","unstructured":"Gyim\u00f3thy, T., Besz\u00e9des, \u00c1., Forg\u00e1cs, I.: An efficient relevant slicing method for debugging. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol.\u00a01687, pp. 303\u2013321. Springer, Heidelberg (1999)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-540-31980-1_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Jain","year":"2005","unstructured":"Jain, H., Ivan\u010di\u0107, F., Gupta, A., Ganai, M.: Localization and register sharing for predicate abstraction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 394\u2013409. Springer, Heidelberg (2005)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_15","volume-title":"Computer Aided Verification","author":"H. Jain","year":"2006","unstructured":"Jain, H., Ivan\u010di\u0107, F., Gupta, A., Shlyakhter, I., Wang, C.: Using statically computed invariants inside the predicate abstraction and refinement loop. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, Springer, Heidelberg (2006)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Computer Aided Verification","author":"B. Jobstmann","year":"2005","unstructured":"Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 226\u2013238. Springer, Heidelberg (2005)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Jones, J.A., Harrold, M.J., Stasko, J.: Visualization of test information to assist fault localization. In: ACM\/IEEE International Conference on Software Engineering (2002)","DOI":"10.1145\/581396.581397"},{"issue":"3","key":"9_CR17","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/0164-1212(90)90094-3","volume":"13","author":"B. Korel","year":"1990","unstructured":"Korel, B., Laski, J.W.: Dynamic slicing of computer programs. Journal of Systems and Software\u00a013(3), 187\u2013195 (1990)","journal-title":"Journal of Systems and Software"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-48153-2_8","volume-title":"Correct Hardware Design and Verification Methods","author":"O. Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 82\u201396. Springer, Heidelberg (1999)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-36577-X_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/10722167_33","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 435\u2013449. Springer, Heidelberg (2000)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","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)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proceedings of the Fifth Annual Symposium on Programming (1981)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Renieris, M., Reiss, S.P.: Fault localization with nearest neighbor queries. In: International Conference on Automated Software Engineering, Montreal, Canada, October 2003, pp. 30\u201339 (2003)","DOI":"10.1109\/ASE.2003.1240292"},{"key":"9_CR24","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/32.689399","volume":"24","author":"G. Rothermel","year":"1999","unstructured":"Rothermel, G., Harrold, M.J.: Empirical studies of a safe regression test selection technique. Software Engineering\u00a024, 401\u2013419 (1999)","journal-title":"Software Engineering"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/11560548_6","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Staber","year":"2005","unstructured":"Staber, S., Jobstmann, B., Bloem, R.: Finding and fixing faults. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 35\u201349. Springer, Heidelberg (2005)"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45661-9_1","volume-title":"Fast Software Encryption","author":"A. Zeller","year":"2002","unstructured":"Zeller, A.: Isolating cause-effect chains from computer programs. In: Daemen, J., Rijmen, V. (eds.) FSE 2002. LNCS, vol.\u00a02365, pp. 1\u201310. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901914_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T14:56:17Z","timestamp":1605624977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901914_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540472377","9783540472384"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11901914_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}