{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T05:01:04Z","timestamp":1725858064525},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319411347"},{"type":"electronic","value":"9783319411354"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-41135-4_9","type":"book-chapter","created":{"date-parts":[[2016,6,20]],"date-time":"2016-06-20T12:23:38Z","timestamp":1466425418000},"page":"151-168","source":"Crossref","is-referenced-by-count":8,"title":["Classifying Bugs with Interpolants"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Podelski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Sch\u00e4f","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,21]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Anvik, J., Hiew, L., Murphy, G.C.: Who should fix this bug? In: ICSE, pp. 361\u2013370. ACM (2006)","DOI":"10.1145\/1134285.1134336"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/978-3-319-06200-6_27","volume-title":"NASA Formal Methods","author":"S Arlt","year":"2014","unstructured":"Arlt, S., Rubio-Gonz\u00e1lez, C., R\u00fcmmer, P., Sch\u00e4f, M., Shankar, N.: The gradual verifier. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 313\u2013327. Springer, Heidelberg (2014)"},{"key":"9_CR3","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/640128.604140","volume":"38","author":"T Ball","year":"2003","unstructured":"Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. SIGPLAN Not. 38, 97\u2013105 (2003)","journal-title":"SIGPLAN Not."},{"issue":"6","key":"9_CR4","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1145\/1953122.1953145","volume":"54","author":"M Barnett","year":"2011","unstructured":"Barnett, M., F\u00e4hndrich, M., Leino, K.R.M., M\u00fcller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Commun. ACM 54(6), 81\u201391 (2011)","journal-title":"Commun. ACM"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/978-3-319-11164-3_14","volume-title":"Runtime Verification","author":"M Tabaei Befrouei","year":"2014","unstructured":"Tabaei Befrouei, M., Wang, C., Weissenbacher, G.: Abstraction and mining of traces to explain concurrency bugs. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 162\u2013177. Springer, Heidelberg (2014)"},{"key":"9_CR6","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Model Theory","author":"C Chang","year":"1990","unstructured":"Chang, C., Keisler, H.J.: Model Theory. Studies in Logic and the Foundations of Mathematics. Elsevier Science, North-Holland (1990)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-3-642-35873-9_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Christ","year":"2013","unstructured":"Christ, J., Ermis, E., Sch\u00e4f, M., Wies, T.: Flow-sensitive fault localization. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 189\u2013208. Springer, Heidelberg (2013)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1007\/978-3-642-20398-5_35","volume-title":"NASA Formal Methods","author":"DR Cok","year":"2011","unstructured":"Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472\u2013479. Springer, Heidelberg (2011)"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282. ACM (1979)","DOI":"10.1145\/567752.567778"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/978-3-642-35873-9_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cousot","year":"2013","unstructured":"Cousot, P., Cousot, R., F\u00e4hndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 128\u2013148. Springer, Heidelberg (2013)"},{"key":"9_CR11","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Automated error diagnosis using abductive inference. In: PLDI, pp. 181\u2013192 (2012)","DOI":"10.1145\/2254064.2254087"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"623","DOI":"10.1007\/978-3-642-36742-7_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Falke","year":"2013","unstructured":"Falke, S., Merz, F., Sinz, C.: LLBMC: improved bounded model checking of $$\\sf C$$ programs using LLVM. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 623\u2013626. Springer, Heidelberg (2013)"},{"key":"9_CR15","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/543552.512558","volume":"37","author":"C Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. SIGPLAN Not. 37, 234\u2013245 (2002)","journal-title":"SIGPLAN Not."},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Gupta, A., Henzinger, T.A., Radhakrishna, A., Samanta, R., Tarrach, T.: Succinct representation of concurrent trace sets. In: POPL, pp. 433\u2013444. ACM (2015)","DOI":"10.1145\/2676726.2677008"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013)"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Jin, W., Orso, A.: Bugredux: reproducing field failures for in-house debugging. In: ICSE, pp. 474\u2013484. IEEE (2012)","DOI":"10.1109\/ICSE.2012.6227168"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Kremenek, T., Engler, D.: Z-ranking: using statistical analysis to counter the impact of static analysis approximations. In: SAS, pp. 295\u2013315 (2003)","DOI":"10.1007\/3-540-44898-5_16"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014)"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S.: Powering the static driver verifier using corral. In: FSE, pp. 202\u2013212. ACM (2014)","DOI":"10.1145\/2635868.2635894"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Le, W., Soffa, M.L.: Path-based fault correlations. In: FSE, pp. 307\u2013316 (2010)","DOI":"10.1145\/1882291.1882336"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/978-3-642-27940-9_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"W Lee","year":"2012","unstructured":"Lee, W., Lee, W., Yi, K.: Sound non-statistical clustering of static analysis alarms. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 299\u2013314. Springer, Heidelberg (2012)"},{"key":"9_CR24","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345, 101\u2013121 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1007\/978-3-319-12154-3_17","volume-title":"Verified Software: Theories, Tools and Experiments","author":"V Murali","year":"2014","unstructured":"Murali, V., Sinha, N., Torlak, E., Chandra, S.: What gives? a hybrid algorithm for error trace explanation. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 270\u2013286. Springer, Heidelberg (2014)"},{"issue":"4","key":"9_CR26","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/69558.69559","volume":"11","author":"G Nelson","year":"1989","unstructured":"Nelson, G.: A generalization of Dijkstra\u2019s calculus. ACM Trans. Program. Lang. Syst. 11(4), 517\u2013561 (1989)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Pacheco, C., Ernst, M.D.: Randoop: feedback-directed random testing for java. In: Companion to the 22nd ACM SIGPLAN Conference on Object-oriented Programming Systems and Applications Companion, OOPSLA 2007, New York, NY, USA, pp. 815\u2013816. ACM (2007)","DOI":"10.1145\/1297846.1297902"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274\u2013289. Springer, Heidelberg (2008)"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: POPL, pp. 318\u2013329. ACM (2004)","DOI":"10.1145\/982962.964028"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Wang, X., Zhang, L., Xie, T., Anvik, J., Sun, J.: An approach to detecting duplicate bug reports using natural language and execution information. In: ICSE, pp. 461\u2013470. ACM (2008)","DOI":"10.1145\/1368088.1368151"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Zeller, A.: Isolating cause-effect chains from computer programs. In: SIGSOFT FSE, pp. 1\u201310 (2002)","DOI":"10.1145\/587051.587053"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41135-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T12:44:32Z","timestamp":1498308272000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41135-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319411347","9783319411354"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41135-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}