{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:41:47Z","timestamp":1742960507211,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319121536"},{"type":"electronic","value":"9783319121543"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12154-3_17","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T08:20:23Z","timestamp":1413188423000},"page":"270-286","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["What Gives? A Hybrid Algorithm for Error Trace Explanation"],"prefix":"10.1007","author":[{"given":"Vijayaraghavan","family":"Murali","sequence":"first","affiliation":[]},{"given":"Nishant","family":"Sinha","sequence":"additional","affiliation":[]},{"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[]},{"given":"Satish","family":"Chandra","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,10,14]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Agrawal, H., Horgan, J.R.: Dynamic program slicing. In: PLDI \u201990, pp. 246\u2013256 (1990)","DOI":"10.1145\/93548.93576"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-30557-6_14","volume-title":"Practical Aspects of Declarative Languages","author":"J Bailey","year":"2005","unstructured":"Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol. 3350, pp. 174\u2013186. Springer, Heidelberg (2005)"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. In: POPL \u201903, pp. 97\u2013105 (2003)","DOI":"10.1145\/640128.604140"},{"key":"17_CR4","first-page":"123","volume":"8","author":"A Belov","year":"2012","unstructured":"Belov, A., Marques-Silva, J.: MUSer2: An efficient MUS extractor. JSAT 8, 123\u2013128 (2012)","journal-title":"JSAT"},{"issue":"5","key":"17_CR5","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST: Applications to software engineering. Int. J. Softw. Tools Technol. Transf. 9(5), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Chandra, S., Torlak, E., Barman, S., Bodik, R.: Angelic debugging. In: ICSE (2011)","DOI":"10.1145\/1985793.1985811"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Cleve, H., Zeller, A.: Locating causes of program failures. In: ICSE, pp. 342\u2013351 (2005)","DOI":"10.1145\/1062455.1062522"},{"key":"17_CR8","first-page":"250","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Comput. 22, 250\u2013268 (1957)","journal-title":"J. Symb. Comput."},{"key":"17_CR9","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1997","unstructured":"Dijkstra, E.W.: A Discipline of Programming, 1st edn. Prentice Hall PTR, Upper Saddle River, NJ, USA (1997)","edition":"1"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Automated error diagnosis using abductive inference. In: PLDI (2012)","DOI":"10.1145\/2254064.2254087"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-11319-2_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V D\u2019Silva","year":"2010","unstructured":"D\u2019Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 129\u2013145. Springer, Heidelberg (2010)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-32759-9_17","volume-title":"FM 2012: Formal Methods","author":"E Ermis","year":"2012","unstructured":"Ermis, E., Sch\u00e4f, M., Wies, T.: Error invariants. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 187\u2013201. Springer, Heidelberg (2012)"},{"key":"17_CR13","doi-asserted-by":"publisher","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.: Error explanation with distance metrics. Softw. Tools Technol. Transf. (STTT) 8, 229\u2013247 (2006)","journal-title":"Softw. Tools Technol. Transf. (STTT)"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Hangal, S., Lam, M.S.: Tracking down software bugs using automatic anomaly detection. In: ICSE \u201902 (2002)","DOI":"10.1145\/581376.581377"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL (2004)","DOI":"10.1145\/964001.964021"},{"issue":"3","key":"17_CR16","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1145\/129393.129398","volume":"14","author":"J Jaffar","year":"1992","unstructured":"Jaffar, J., Michaylov, S., Stuckey, P.J., Yap, R.H.C.: The CLP($$\\cal {R}$$) language and system. ACM Trans. Program. Lang. Syst. 14(3), 339\u2013395 (1992)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1007\/978-3-642-31424-7_61","volume-title":"Computer Aided Verification","author":"J Jaffar","year":"2012","unstructured":"Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: TRACER: A Symbolic execution tool for verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 758\u2013766. Springer, Heidelberg (2012)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Jones, J.A., Harrold, M.J., Stasko, J.: Visualization of test information to assist fault localization. In: ICSE \u201902, pp. 467\u2013477 (2002)","DOI":"10.1145\/581396.581397"},{"issue":"6","key":"17_CR20","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1145\/1993316.1993550","volume":"46","author":"M Jose","year":"2011","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: Error localization using maximum satisfiability. SIGPLAN Not. 46(6), 437\u2013446 (2011)","journal-title":"SIGPLAN Not."},{"issue":"1","key":"17_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1\u201333 (2008)","journal-title":"J. Autom. Reason."},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Logozzo, F., Ball, T.: Modular and verified automatic program repair. In: OOPSLA (2012)","DOI":"10.1145\/2384616.2384626"},{"key":"17_CR23","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/S0049-237X(08)72018-4","volume-title":"Computer Programming and Formal Systems","author":"J McCarthy","year":"1963","unstructured":"McCarthy, J.: A basis for a mathematical theory of computation. In: Braffort, P., Hirshberg, D. (eds.) Computer Programming and Formal Systems, pp. 33\u201370. North-Holland, Amsterdam (1963)"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-Based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of Craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1\u201312. Springer, Heidelberg (2005)"},{"key":"17_CR26","unstructured":"Nadel, A.: Boosting minimal unsatisfiable core extraction. In: FMCAD (2010)"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"GC Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Nigel Horspool, R. (ed.) CC 2002. LNCS, vol. 2304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"issue":"3","key":"17_CR28","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/2211616.2211622","volume":"21","author":"D Qi","year":"2012","unstructured":"Qi, D., Roychoudhury, A., Liang, Z., Vaswani, K.: Darwin: An approach to debugging evolving programs. ACM Trans. Softw. Eng. Methodol. 21(3), 19 (2012)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-31424-7_18","volume-title":"Computer Aided Verification","author":"SF Rollini","year":"2012","unstructured":"Rollini, S.F., Sery, O., Sharygina, N.: Leveraging interpolant strength in model checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 193\u2013209. Springer, Heidelberg (2012)"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Sahoo, S.K., Criswell, J., Geigle, C., Adve, V.: Using likely invariants for automated software fault localization. In: ASPLOS (2013)","DOI":"10.1145\/2451116.2451131"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Sch\u00e4f, M., Schwartz-Narbonne, D., Wies, T.: Explaining inconsistent code. In: ESEC\/SIGSOFT FSE, pp. 521\u2013531 (2013)","DOI":"10.1145\/2491411.2491448"},{"key":"17_CR32","unstructured":"Silva, J.P.M.: Minimal unsatisfiability: Models, algorithms and applications (invited paper). In: ISMVL (2010)"},{"key":"17_CR33","unstructured":"Software-artifact infrastructure repository (SIR), August 2010. http:\/\/sir.unl.edu\/portal\/index.html"},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"Vizel, Y., Grumberg, O.: Interpolation-sequence based model checking. In: FMCAD (2009)","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"17_CR35","doi-asserted-by":"crossref","unstructured":"Zeller, A.: Isolating cause-effect chains from computer programs. In: FSE \u201902, pp. 1\u201310 (2002)","DOI":"10.1145\/587051.587053"},{"issue":"2","key":"17_CR36","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10664-006-9007-3","volume":"12","author":"X Zhang","year":"2007","unstructured":"Zhang, X., Gupta, N., Gupta, R.: A study of effectiveness of dynamic slicing in locating real faults. Empir. Softw. Engg. 12(2), 143\u2013160 (2007)","journal-title":"Empir. Softw. Engg."}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12154-3_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T14:44:29Z","timestamp":1676904269000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-12154-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319121536","9783319121543"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12154-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"14 October 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}