{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T02:34:36Z","timestamp":1774060476654,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642541070","type":"print"},{"value":"9783642541087","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54108-7_1","type":"book-chapter","created":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T05:09:36Z","timestamp":1389762576000},"page":"1-21","source":"Crossref","is-referenced-by-count":18,"title":["Classifying and Solving Horn Clauses for Verification"],"prefix":"10.1007","author":[{"given":"Philipp","family":"R\u00fcmmer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hossein","family":"Hojjat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_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":"1_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":"1_CR3","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.\u00a07358, pp. 672\u2013678. Springer, Heidelberg (2012)"},{"key":"1_CR4","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":"1_CR5","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The smt-lib standard: Version 2.0. Technical report (2010)"},{"key":"1_CR6","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: SMT Workshop at IJCAR (2012)"},{"key":"1_CR7","unstructured":"Bonacina, M.P., Johansson, M.: On interpolation in automated theorem proving (2012) (submitted)"},{"key":"1_CR8","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":"1_CR9","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":"1_CR10","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":"1_CR11","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. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"8","key":"1_CR12","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM\u00a022(8), 465\u2013476 (1979)","journal-title":"Commun. ACM"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Ferm\u00fcller, C., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 25, pp. 1791\u20131850. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50027-8"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: CAV 1997, pp. 72\u201383 (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"1_CR15","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":"1_CR16","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":"1_CR17","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":"1_CR18","doi-asserted-by":"crossref","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Generalised interpolation by solving recursion-free horn clauses. CoRR, abs\/1303.7378 (2013)","DOI":"10.4204\/EPTCS.169.5"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: POPL (2010)","DOI":"10.1145\/1706299.1706353"},{"key":"1_CR20","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\/982962.964021"},{"key":"1_CR21","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":"1_CR22","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)"},{"issue":"1","key":"1_CR23","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1145\/322047.322059","volume":"25","author":"H.R. Lewis","year":"1978","unstructured":"Lewis, H.R.: Renaming a set of clauses as a Horn set. J. ACM\u00a025(1), 134\u2013135 (1978)","journal-title":"J. ACM"},{"key":"1_CR24","unstructured":"McMillan, K.L.: iZ3 documentation, http:\/\/research.microsoft.com\/en-us\/um\/redmond\/projects\/z3\/iz3documentation.html"},{"key":"1_CR25","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":"1_CR26","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":"K.L. 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.\u00a03440, pp. 1\u201312. Springer, Heidelberg (2005)"},{"key":"1_CR27","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":"1_CR28","unstructured":"McMillan, K.L., Rybalchenko, A.: Solving constrained Horn clauses using interpolation. Technical Report MSR-TR-2013-6 (January 2013), http:\/\/research.microsoft.com\/apps\/pubs\/default.aspx?id=180055"},{"key":"1_CR29","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.A., 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":"1_CR30","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report). ArXiv e-prints (January 2013), http:\/\/arxiv.org\/abs\/1301.4973","DOI":"10.1007\/978-3-642-39799-8_24"},{"key":"1_CR31","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":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-23702-7_23","volume-title":"Static Analysis","author":"P. Suter","year":"2011","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) Static Analysis. LNCS, vol.\u00a06887, pp. 298\u2013315. Springer, Heidelberg (2011)"},{"issue":"1","key":"1_CR33","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/s10515-006-0005-x","volume":"14","author":"M. Taghdiri","year":"2007","unstructured":"Taghdiri, M., Jackson, D.: Inferring specifications to detect errors in code. Autom. Softw. Eng.\u00a014(1), 87\u2013121 (2007)","journal-title":"Autom. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54108-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,23]],"date-time":"2022-03-23T12:32:27Z","timestamp":1648038747000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54108-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642541070","9783642541087"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54108-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}