{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:14:32Z","timestamp":1725902072287},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_35","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"499-514","source":"Crossref","is-referenced-by-count":3,"title":["Finding Inconsistencies in Programs with Loops"],"prefix":"10.1007","author":[{"given":"Temesghen","family":"Kahsai","sequence":"first","affiliation":[]},{"given":"Jorge A.","family":"Navas","sequence":"additional","affiliation":[]},{"given":"Dejan","family":"Jovanovi\u0107","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Sch\u00e4f","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"35_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1007\/978-3-642-31424-7_48","volume-title":"Computer Aided Verification","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: UFO: a framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 672\u2013678. Springer, Heidelberg (2012)"},{"key":"35_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"35_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-27705-4_24","volume-title":"Verified Software: Theories, Tools, Experiments","author":"C Bertolini","year":"2012","unstructured":"Bertolini, C., Sch\u00e4f, M., Schweitzer, P.: Infeasible code detection. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 310\u2013325. Springer, Heidelberg (2012)"},{"key":"35_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25\u201332 (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"35_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Gurevich Festschrift II 2015. LNCS, vol. 9300, pp. 24\u201351. Springer, Heidelberg (2015)"},{"key":"35_CR6","doi-asserted-by":"crossref","unstructured":"Blackshear, S., Lahiri, S.K.: Almost-correct specifications: a modular semantic framework for assigning confidence to warnings. In: PLDI, pp. 209\u2013218 (2013)","DOI":"10.1145\/2499370.2462188"},{"key":"35_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-31424-7_4","volume-title":"Computer Aided Verification","author":"AR Bradley","year":"2012","unstructured":"Bradley, A.R.: IC3 and beyond: incremental, inductive verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 4\u20134. Springer, Heidelberg (2012)"},{"key":"35_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/978-3-642-54862-8_47","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Angelis De","year":"2014","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: VeriMAP: a tool for verifying programs through transformations. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 568\u2013574. Springer, Heidelberg (2014)"},{"key":"35_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"G Delzanno","year":"1999","unstructured":"Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 223\u2013239. Springer, Heidelberg (1999)"},{"key":"35_CR10","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Static error detection using semantic inconsistency inference. In: PLDI, pp. 435\u2013445 (2007)","DOI":"10.1145\/1273442.1250784"},{"key":"35_CR11","doi-asserted-by":"crossref","unstructured":"Engler, D., Chen, D.Y., Hallem, S., Chou, A., Chelf, B.: Bugs as deviant behavior: a general approach to inferring errors in systems code. In: SOSP (2001)","DOI":"10.21236\/ADA419584"},{"key":"35_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)"},{"issue":"1\u20133","key":"35_CR13","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.scico.2004.01.006","volume":"50","author":"C Flanagan","year":"2004","unstructured":"Flanagan, C.: Automatic software model checking via constraint logic. Sci. Comput. Program. 50(1\u20133), 253\u2013270 (2004)","journal-title":"Sci. Comput. Program."},{"key":"35_CR14","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405\u2013416 (2012)","DOI":"10.1145\/2345156.2254112"},{"key":"35_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-20398-5_11","volume-title":"NASA Formal Methods","author":"A Gurfinkel","year":"2011","unstructured":"Gurfinkel, A., Chaki, S., Sapra, S.: Efficient predicate abstraction of program summaries. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 131\u2013145. Springer, Heidelberg (2011)"},{"key":"35_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Heidelberg (2015)"},{"key":"35_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012)"},{"key":"35_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-05089-3_22","volume-title":"FM 2009: Formal Methods","author":"J Hoenicke","year":"2009","unstructured":"Hoenicke, J., Leino, K.R.M., Podelski, A., Sch\u00e4f, M., Wies, T.: It\u2019s doomed; we can prove it. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 338\u2013353. Springer, Heidelberg (2009)"},{"key":"35_CR19","doi-asserted-by":"crossref","unstructured":"Hoenicke, J., Leino, K.R.M., Podelski, A., Sch\u00e4f, M., Wies, T.: Doomed program points. In: FMSD, pp. 171\u2013199 (2010)","DOI":"10.1007\/s10703-010-0102-0"},{"key":"35_CR20","doi-asserted-by":"crossref","unstructured":"Hovemeyer, D., Pugh, W.: Finding more null pointer bugs, but not too many. In: PASTE, pp. 9\u201314 (2007)","DOI":"10.1145\/1251535.1251537"},{"key":"35_CR21","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":"35_CR22","doi-asserted-by":"crossref","unstructured":"Janota, M., Grigore, R., Moskal, M.: Reachability analysis for annotated code. In: SAVCBS, pp. 23\u201330 (2007)","DOI":"10.1145\/1292316.1292319"},{"key":"35_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-22110-1_40","volume-title":"Computer Aided Verification","author":"M Jose","year":"2011","unstructured":"Jose, M., Majumdar, R.: Bug-assist: assisting fault localization in ANSI-C programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 504\u2013509. Springer, Heidelberg (2011)"},{"key":"35_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2014","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17\u201334. Springer, Heidelberg (2014)"},{"key":"35_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"846","DOI":"10.1007\/978-3-642-39799-8_59","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2013","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 846\u2013862. Springer, Heidelberg (2013)"},{"key":"35_CR26","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: Automatic pool allocation: improving performance by controlling data structure layout in the heap. In: PLDI, pp. 129\u2013142 (2005)","DOI":"10.1145\/1064978.1065027"},{"key":"35_CR27","doi-asserted-by":"crossref","unstructured":"McCarthy, T., R\u00fcmmer, P., Sch\u00e4f, M.: Bixie: finding and understanding inconsistent code. In: ICSE, pp. 645\u2013648 (2015)","DOI":"10.1109\/ICSE.2015.213"},{"key":"35_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-49727-7_15","volume-title":"Static Analysis","author":"JC Peralta","year":"1998","unstructured":"Peralta, J.C., Gallagher, J.P., Saglam, H.: Analysis of imperative programs through analysis of constraint logic programs. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 246\u2013261. Springer, Heidelberg (1998)"},{"key":"35_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1007\/978-3-642-36742-7_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Popeea","year":"2013","unstructured":"Popeea, C., Rybalchenko, A.: Threader: a verifier for multi-threaded programs. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 633\u2013636. Springer, Heidelberg (2013)"},{"key":"35_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54108-7_1","volume-title":"Verified Software: Theories, Tools, Experiments","author":"P R\u00fcmmer","year":"2014","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Classifying and solving horn clauses for verification. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 1\u201321. Springer, Heidelberg (2014)"},{"key":"35_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-642-39799-8_24","volume-title":"Computer Aided Verification","author":"P R\u00fcmmer","year":"2013","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 347\u2013363. Springer, Heidelberg (2013)"},{"key":"35_CR32","doi-asserted-by":"crossref","unstructured":"Sch\u00e4f, M., Schwartz-Narbonne, D., Wies, T.: Explaining inconsistent code. In: ESEC\/FSE, pp. 521\u2013531 (2013)","DOI":"10.1145\/2491411.2491448"},{"key":"35_CR33","unstructured":"SeaHorn Inconsistency Checker. \n                    https:\/\/github.com\/seahorn\/seahorn\/tree\/inconsistency"},{"key":"35_CR34","doi-asserted-by":"crossref","unstructured":"Tomb, A., Flanagan, C.: Detecting inconsistencies via universal reachability analysis. In: ISSTA, pp. 287\u2013297 (2012)","DOI":"10.1145\/2338965.2336788"},{"issue":"1","key":"35_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2699678","volume":"33","author":"X Wang","year":"2015","unstructured":"Wang, X., Zeldovich, N., Kaashoek, M.F., Solar-Lezama, A.: A differential approach to undefined behavior detection. TOCS 33(1), 1\u201329 (2015)","journal-title":"TOCS"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:28:14Z","timestamp":1559330894000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}