{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,21]],"date-time":"2026-09-21T12:36:37Z","timestamp":1789994197884,"version":"4.0.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319175232","type":"print"},{"value":"9783319175249","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-17524-9_23","type":"book-chapter","created":{"date-parts":[[2015,4,7]],"date-time":"2015-04-07T06:15:31Z","timestamp":1428387331000},"page":"327-342","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Conflict-Directed Graph Coverage"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Schwartz-Narbonne","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Sch\u00e4f","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dejan","family":"Jovanovi\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,4,8]]},"reference":[{"key":"23_CR1","unstructured":"The legion of the bouncy castle. https:\/\/www.bouncycastle.org\/"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1007\/978-3-319-02444-8_44","volume-title":"Automated Technology for Verification and Analysis","author":"S Arlt","year":"2013","unstructured":"Arlt, S., R\u00fcmmer, P., Sch\u00e4f, M.: A theory for control-flow graph exploration. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 506\u2013515. Springer, Heidelberg (2013)"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"767","DOI":"10.1007\/978-3-642-31424-7_62","volume-title":"Computer Aided Verification","author":"S Arlt","year":"2012","unstructured":"Arlt, S., Sch\u00e4f, M.: Joogie: infeasible code detection for java. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 767\u2013773. Springer, Heidelberg (2012)"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. SIGPLAN Not., 97\u2013105 (2003)","DOI":"10.1145\/640128.604140"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. SIGSOFT Softw. Eng. Notes, 82\u201387 (2005)","DOI":"10.1145\/1108768.1108813"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. ACM SIGSOFT Software Engineering Notes 31, 82\u201387 (2005)","DOI":"10.1145\/1108768.1108813"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 1254, pp. 279\u2013290. Springer, Heidelberg (1997)"},{"key":"23_CR9","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":"23_CR10","unstructured":"Bj\u00f8rner, N., Dutertre, B., de Moura, L.: Accelerating lemma learning using joins-DPLL (join). In: Int. Conf. Logic for Programming, Artif. Intell. and Reasoning, LPAR (2008)"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/3-540-45319-9_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage metrics for temporal logic model checking. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 528\u2013542. Springer, Heidelberg (2001)"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. TOPLAS, 451\u2013490 (1991)","DOI":"10.1145\/115372.115320"},{"key":"23_CR13","unstructured":"de Moura, L., Bj\u00f8rner, N.: Relevancy propagation. Technical Report MSR-TR-2007-140, Microsoft Research (2007)"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Static error detection using semantic inconsistency inference. In: PLDI (2007)","DOI":"10.1145\/1250734.1250784"},{"key":"23_CR16","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: Proceedings of the Eighteenth ACM Symposium on Operating Systems Principles, SOSP 2001, pp. 57\u201372. ACM, New York (2001)","DOI":"10.1145\/502059.502041"},{"key":"23_CR17","unstructured":"Gheorghiu, M., Gurfinkel, A.: Vaquot: A tool for vacuity detection. Technical report. In: Proceedings of Tool Track, FM 2006 (2005)"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Hoenicke, J., Leino, K.R., Podelski, A., Sch\u00e4f, M., Wies, T.: Doomed program points. Formal Methods in System Design (2010)","DOI":"10.1007\/s10703-010-0102-0"},{"issue":"12","key":"23_CR19","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1052883.1052895","volume":"39","author":"D Hovemeyer","year":"2004","unstructured":"Hovemeyer, D., Pugh, W.: Finding bugs is easy. ACM Sigplan Notices 39(12), 92\u2013106 (2004)","journal-title":"ACM Sigplan Notices"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Janota, M., Grigore, R., Moskal, M.: Reachability analysis for annotated code. In: SAVCBS (2007)","DOI":"10.1145\/1292316.1292319"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Symposium on the Complexity of Computer Computations, The IBM Research Symposia Series, pp. 85\u2013103. Plenum Press, New York (1972)","DOI":"10.1007\/978-1-4684-2001-2_9"},{"issue":"1\u20133","key":"23_CR22","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.scico.2004.05.016","volume":"55","author":"KRM Leino","year":"2005","unstructured":"Leino, K.R.M., Millstein, T.D., Saxe, J.B.: Generating error traces from verification-condition counterexamples. Sci. Comput. Program. 55(1\u20133), 209\u2013226 (2005)","journal-title":"Sci. Comput. Program."},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-12002-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: A Polymorphic intermediate verification language: design and logical encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 312\u2013327. Springer, Heidelberg (2010)"},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","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, vol. 5330, pp. 274\u2013289. Springer, Heidelberg (2008)"},{"key":"23_CR25","unstructured":"Sch\u00e4f, M.: Bixie: Find contradictions in java code (2014). http:\/\/www.csl.sri.com\/bixie-ws\/"},{"key":"23_CR26","unstructured":"Sch\u00e4f, M.: Gravy website (2014). https:\/\/github.com\/martinschaef\/gravy"},{"key":"23_CR27","unstructured":"Silva, J.P.M., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 131\u2013153. IOS Press (2009)"},{"key":"23_CR28","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"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"Wang, X., Zeldovich, N., Kaashoek, M.F., Solar-Lezama, A.: Towards optimization-safe systems: analyzing the impact of undefined behavior. In: SOSP, pp. 260\u2013275. ACM (2013)","DOI":"10.1145\/2517349.2522728"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17524-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T07:28:48Z","timestamp":1676446128000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17524-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175232","9783319175249"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17524-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"8 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}