{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:10:04Z","timestamp":1784844604077,"version":"3.55.0"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,12,3]],"date-time":"2014-12-03T00:00:00Z","timestamp":1417564800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2015,8]]},"DOI":"10.1007\/s10703-014-0219-7","type":"journal-article","created":{"date-parts":[[2014,12,2]],"date-time":"2014-12-02T18:35:31Z","timestamp":1417545331000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["On recursion-free Horn clauses and Craig interpolation"],"prefix":"10.1007","volume":"47","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","published-online":{"date-parts":[[2014,12,3]]},"reference":[{"key":"219_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi A, Gurfinkel A, Chechik M (2012) Craig interpretation. In: SAS","DOI":"10.1007\/978-3-642-33125-1_21"},{"key":"219_CR2","doi-asserted-by":"crossref","unstructured":"Albarghouthi A, Gurfinkel A, Chechik M (2012) Whale: an interpolation-based algorithm for inter-procedural verification. In: VMCAI, pp 39\u201355","DOI":"10.1007\/978-3-642-27940-9_4"},{"key":"219_CR3","doi-asserted-by":"crossref","unstructured":"Ball T, Podelski, A, Rajamani SK (2002) Relative completeness of abstraction refinement for software model checking. In: TACAS\u201902, LNCS, vol 2280, p 158","DOI":"10.1007\/3-540-46002-0_12"},{"key":"219_CR4","doi-asserted-by":"crossref","unstructured":"Banda G, Gallagher JP (2009) Analysis of linear hybrid systems in clp. In: Hanus [20], pp 55\u201370. doi: 10.1007\/978-3-642-00515-2_5","DOI":"10.1007\/978-3-642-00515-2_5"},{"key":"219_CR5","doi-asserted-by":"crossref","unstructured":"Beyene TA, Popeea C, Rybalchenko A (2013) Solving existentially quantified Horn clauses. In: CAV","DOI":"10.1007\/978-3-642-39799-8_61"},{"key":"219_CR6","unstructured":"Beyer D (2014) Status report on software verification\u2014(competition summary sv-comp 2014). In: TACAS, pp 373\u2013388"},{"key":"219_CR7","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner N, McMillan KL, Rybalchenko A (2013) On solving universally quantified Horn clauses. In: SAS","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"219_CR8","doi-asserted-by":"crossref","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 (2011) An interpolating sequent calculus for quantifier-free Presburger arithmetic. J Autom Reason 47:341\u2013367. doi: 10.1007\/s10817-011-9237-y","journal-title":"J Autom Reason"},{"issue":"1","key":"219_CR9","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1145\/1838552.1838559","volume":"12","author":"A Cimatti","year":"2010","unstructured":"Cimatti A, Griggio A, Sebastiani R (2010) Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans Comput Log 12(1):7","journal-title":"ACM Trans Comput Log"},{"issue":"3","key":"219_CR10","doi-asserted-by":"crossref","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig W (1957) Linear reasoning. A new form of the Herbrand\u2013Gentzen theorem. J Symb Log 22(3):250\u2013268","journal-title":"J Symb Log"},{"key":"219_CR11","doi-asserted-by":"crossref","unstructured":"Dillig I, Dillig T, Li B, McMillan KL (2013) Inductive invariant generation via abductive inference. In: OOPSLA, pp 443\u2013456","DOI":"10.1145\/2509136.2509511"},{"key":"219_CR12","doi-asserted-by":"crossref","unstructured":"Felsing D, Grebing S, Klebanov V, R\u00fcmmer P, Ulbrich M (2014) Automating regression verification. In: Crnkovic I, Chechik M, Gr\u00fcnbacher P (eds) ACM\/IEEE international conference on automated software engineering, ASE. ACM, New York, pp 349\u2013360","DOI":"10.1145\/2642937.2642987"},{"issue":"2","key":"219_CR13","first-page":"175","volume":"13","author":"F Fioravanti","year":"2013","unstructured":"Fioravanti F, Pettorossi A, Proietti M, Senni V (2013) Generalization strategies for the verification of infinite state systems. TPLP 13(2):175\u2013199. doi: 10.1017\/S1471068411000627","journal-title":"TPLP"},{"key":"219_CR14","doi-asserted-by":"crossref","unstructured":"Godefroid P, Yannakakis M (2013) Analysis of boolean programs. In: TACAS, pp 214\u2013229","DOI":"10.1007\/978-3-642-36742-7_16"},{"key":"219_CR15","doi-asserted-by":"crossref","unstructured":"Graf S, Saidi H (1997) Construction of abstract state graphs with PVS. In: CAV","DOI":"10.1007\/3-540-63166-6_10"},{"key":"219_CR16","doi-asserted-by":"crossref","unstructured":"Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDI","DOI":"10.1145\/2254064.2254112"},{"key":"219_CR17","doi-asserted-by":"crossref","unstructured":"Gupta A, Popeea C, Rybalchenko A (2011) Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL","DOI":"10.1145\/1926385.1926424"},{"key":"219_CR18","doi-asserted-by":"crossref","unstructured":"Gupta A, Popeea C, Rybalchenko A (2011) Solving recursion-free Horn clauses over LI+UIF. In: APLAS, pp 188\u2013203","DOI":"10.1007\/978-3-642-25318-8_16"},{"key":"219_CR19","unstructured":"Gupta A, Popeea C, Rybalchenko A (2013) Generalised interpolation by solving recursion-free Horn clauses. CoRR abs\/1303.7378"},{"key":"219_CR20","unstructured":"Hanus M (ed.) (2009) Logic-based program synthesis and transformation, 18th international symposium, LOPSTR 2008, Valencia, Spain, July 17\u201318, 2008, Revised Selected Papers, Lecture Notes in Computer Science, vol 5438. Springer, Berlin"},{"key":"219_CR21","doi-asserted-by":"crossref","unstructured":"Heizmann M, Hoenicke J, Podelski A (2010) Nested interpolants. In: POPL","DOI":"10.1145\/1706299.1706353"},{"key":"219_CR22","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R, McMillan KL (2004) Abstractions from proofs. In: POPL. ACM, New York, pp 232\u2013244","DOI":"10.1145\/964001.964021"},{"key":"219_CR23","doi-asserted-by":"crossref","unstructured":"Hoder K, Bj\u00f8rner N (2012) Generalized property directed reachability. In: SAT","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"219_CR24","doi-asserted-by":"crossref","unstructured":"Hojjat H, Iosif R, Kone\u010dn\u00fd F, Kuncak V, R\u00fcmmer P (2012) Accelerating interpolants. In: Automated technology for verification and analysis (ATVA)","DOI":"10.1007\/978-3-642-33386-6_16"},{"key":"219_CR25","doi-asserted-by":"crossref","unstructured":"Jhala R, Majumdar R, Rybalchenko A (2011) HMC: Verifying functional programs using abstract interpreters. In: CAV","DOI":"10.1007\/978-3-642-22110-1_38"},{"key":"219_CR26","doi-asserted-by":"crossref","unstructured":"Kafle B, Gallagher JP (2014) Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification. In: Workshop on Horn clauses for verification and synthesis","DOI":"10.4204\/EPTCS.169.7"},{"key":"219_CR27","unstructured":"Kincaid Z LIA Horn benchmarks. https:\/\/svn.sosy-lab.org\/software\/sv-benchmarks\/trunk\/clauses\/LIA\/Zachary\/"},{"key":"219_CR28","doi-asserted-by":"crossref","unstructured":"Komuravelli A, Gurfinkel A, Chaki S (2014) SMT-based model checking for recursive programs. In: Biere A, Bloem R (eds) CAV, Lecture Notes in Computer Science, vol 8559. Springer, Heidelberg, pp 17\u201334","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"219_CR29","doi-asserted-by":"crossref","unstructured":"Komuravelli A, Gurfinkel A, Chaki S, Clarke EM Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina and Veith [42], pp 846\u2013862","DOI":"10.1007\/978-3-642-39799-8_59"},{"key":"219_CR30","doi-asserted-by":"crossref","unstructured":"Lal A, Qadeer S, Lahiri SK (2012) Corral: A solver for reachability modulo theories. In: CAV","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"219_CR31","unstructured":"McMillan KL iZ3 documentation. http:\/\/research.microsoft.com\/en-us\/um\/redmond\/projects\/z3\/iz3documentation.html"},{"key":"219_CR32","doi-asserted-by":"crossref","unstructured":"McMillan KL (2003) Interpolation and SAT-based model checking. In: CAV","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"219_CR33","doi-asserted-by":"crossref","unstructured":"McMillan KL (2006) Lazy abstraction with interpolants. In: CAV","DOI":"10.1007\/11817963_14"},{"key":"219_CR34","unstructured":"McMillan KL, Rybalchenko A (2013) Solving constrained Horn clauses using interpolation. Tech. Rep. MSR-TR-2013-6, Microsoft Research"},{"key":"219_CR35","unstructured":"M\u00e9ndez-Lojo M, Navas JA, Hermenegildo MV (2007) A flexible, (C)LP-based approach to the analysis of object-oriented programs. In: LOPSTR, pp 154\u2013168"},{"key":"219_CR36","doi-asserted-by":"crossref","unstructured":"Peralta JC, Gallagher JP, Saglam H (1998) Analysis of imperative programs through analysis of constraint logic programs. In: SAS","DOI":"10.1007\/3-540-49727-7_15"},{"key":"219_CR37","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer P, Hojjat H, Kuncak V (2013) Classifying and solving Horn clauses for verification. In: VSTTE","DOI":"10.1007\/978-3-642-54108-7_1"},{"key":"219_CR38","unstructured":"R\u00fcmmer P, Hojjat H, Kuncak V (2013) Classifying and solving Horn clauses for verification. In: Cohen E, Rybalchenko A (eds.) VSTTE, Lecture Notes in Computer Science, vol 8164. Springer, Heidelberg, pp 1\u201321"},{"key":"219_CR39","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer P, Hojjat H, Kuncak V Disjunctive interpolants for Horn-clause verification. In: Sharygina and Veith [42], pp 347\u2013363","DOI":"10.1007\/978-3-642-39799-8_24"},{"key":"219_CR40","unstructured":"R\u00fcmmer P, Hojjat H, Kuncak V (2013) Disjunctive interpolants for Horn-Clause verification (Extended Technical Report). ArXiv e-prints (2013). http:\/\/arxiv.org\/abs\/1301.4973"},{"key":"219_CR41","unstructured":"Sery O, Fedyukovich G, Sharygina N (2011) Interpolation-based function summaries in bounded model checking. In: Haifa verification conference, pp 160\u2013175"},{"key":"219_CR42","doi-asserted-by":"crossref","unstructured":"Sharygina N, Veith H (eds) (2013) Computer aided verification\u201425th international conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings, Lecture Notes in Computer Science, vol 8044. Springer","DOI":"10.1007\/978-3-642-39799-8"},{"key":"219_CR43","doi-asserted-by":"crossref","unstructured":"Terauchi T (2010) Dependent types from counterexamples. In: POPL, pp 119\u2013130","DOI":"10.1145\/1706299.1706315"},{"key":"219_CR44","doi-asserted-by":"crossref","unstructured":"Unno H, Terauchi T, Kobayashi N (2013) Automating relatively complete verification of higher-order functional programs. In: POPL","DOI":"10.1145\/2429069.2429081"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0219-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-014-0219-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0219-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,18]],"date-time":"2019-08-18T02:37:32Z","timestamp":1566095852000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-014-0219-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,3]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["219"],"URL":"https:\/\/doi.org\/10.1007\/s10703-014-0219-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12,3]]}}}