{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T02:21:13Z","timestamp":1785291673654,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642397981","type":"print"},{"value":"9783642397998","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_24","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T19:13:06Z","timestamp":1373483586000},"page":"347-363","source":"Crossref","is-referenced-by-count":52,"title":["Disjunctive Interpolants for Horn-Clause Verification"],"prefix":"10.1007","author":[{"given":"Philipp","family":"R\u00fcmmer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hossein","family":"Hojjat","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-642-33125-1_21","volume-title":"Static Analysis","author":"A. Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: Craig interpretation. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 300\u2013316. Springer, Heidelberg (2012)"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-27940-9_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: whale: An interpolation-based algorithm for inter-procedural verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 39\u201355. Springer, Heidelberg (2012)"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-46002-0_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2002","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 158\u2013172. Springer, Heidelberg (2002)"},{"key":"24_CR4","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s10817-011-9237-y","volume":"47","author":"A. Brillout","year":"2011","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free Presburger arithmetic. Journal of Automated Reasoning\u00a047, 341\u2013367 (2011)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"24_CR5","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/1838552.1838559","volume":"12","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log.\u00a012(1), 7 (2010)","journal-title":"ACM Trans. Comput. Log."},{"issue":"3","key":"24_CR6","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. The Journal of Symbolic Logic\u00a022(3), 250\u2013268 (1957)","journal-title":"The Journal of Symbolic Logic"},{"key":"24_CR7","unstructured":"Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. CoRR, abs\/1011.0551 (2010)"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL (2011)","DOI":"10.1145\/1926385.1926424"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-25318-8_16","volume-title":"Programming Languages and Systems","author":"A. Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Solving recursion-free horn clauses over LI+UIF. In: Yang, H. (ed.) APLAS 2011. LNCS, vol.\u00a07078, pp. 188\u2013203. Springer, Heidelberg (2011)"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: POPL (2010)","DOI":"10.1145\/1706299.1706353"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244. ACM (2004)","DOI":"10.1145\/964001.964021"},{"key":"24_CR14","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.\u00a07317, pp. 157\u2013171. Springer, Heidelberg (2012)"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-33386-6_16","volume-title":"Automated Technology for Verification and Analysis","author":"H. Hojjat","year":"2012","unstructured":"Hojjat, H., Iosif, R., Kone\u010dn\u00fd, F., Kuncak, V., R\u00fcmmer, P.: Accelerating interpolants. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 187\u2013202. Springer, Heidelberg (2012)"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-32759-9_21","volume-title":"FM 2012: Formal Methods","author":"H. Hojjat","year":"2012","unstructured":"Hojjat, H., Kone\u010dn\u00fd, F., Garnier, F., Iosif, R., Kuncak, V., R\u00fcmmer, P.: A verification toolkit for numerical transition systems (tool paper). In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol.\u00a07436, pp. 247\u2013251. Springer, Heidelberg (2012)"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-22110-1_38","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2011","unstructured":"Jhala, R., Majumdar, R., Rybalchenko, A.: HMC: Verifying functional programs using abstract interpreters. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 470\u2013485. Springer, Heidelberg (2011)"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-31424-7_32","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2012","unstructured":"Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 427\u2013443. Springer, Heidelberg (2012)"},{"key":"24_CR19","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":"K.L. 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.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"24_CR21","unstructured":"McMillan, K.L., Rybalchenko, A.: Solving constrained Horn clauses using interpolation. Technical Report MSR-TR-2013-6, Microsoft Research (January 2013)"},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-78769-3_11","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M. M\u00e9ndez-Lojo","year":"2008","unstructured":"M\u00e9ndez-Lojo, M., Navas, J., Hermenegildo, M.V.: A flexible (C)LP-based approach to the analysis of object-oriented programs. In: King, A. (ed.) LOPSTR 2007. LNCS, vol.\u00a04915, pp. 154\u2013168. Springer, Heidelberg (2008)"},{"key":"24_CR23","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":"J.C. 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.\u00a01503, pp. 246\u2013261. Springer, Heidelberg (1998)"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Classifying and solving horn clauses for verification. In: VSTTE (2013)","DOI":"10.1007\/978-3-642-54108-7_1"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification (extended technical report). CoRR, abs\/1301.4973 (2013)","DOI":"10.1007\/978-3-642-39799-8_24"},{"key":"24_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-34188-5_15","volume-title":"Hardware and Software: Verification and Testing","author":"O. Sery","year":"2012","unstructured":"Sery, O., Fedyukovich, G., Sharygina, N.: Interpolation-based function summaries in bounded model checking. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol.\u00a07261, pp. 160\u2013175. Springer, Heidelberg (2012)"},{"key":"24_CR27","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: Dependent types from counterexamples. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL, pp. 119\u2013130. ACM (2010)","DOI":"10.1145\/1706299.1706315"},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"Unno, H., Terauchi, T., Kobayashi, N.: Automating relatively complete verification of higher-order functional programs. In: POPL (2013)","DOI":"10.1145\/2429069.2429081"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,17]],"date-time":"2019-07-17T20:58:03Z","timestamp":1563397083000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}