{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T11:02:13Z","timestamp":1740135733575,"version":"3.37.3"},"reference-count":36,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2018,5,11]],"date-time":"2018-05-11T00:00:00Z","timestamp":1525996800000},"content-version":"unspecified","delay-in-days":71,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2018,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we show how the notion of tree dimension can be used in the verification of constrained Horn clauses (CHCs). The dimension of a tree is a numerical measure of its branching complexity and the concept here applies to Horn clause derivation trees. Derivation trees of dimension zero correspond to derivations using linear CHCs, while trees of higher dimension arise from derivations using non-linear CHCs. We show how to instrument CHCs predicates with an extra argument for the dimension, allowing a CHC verifier to reason about bounds on the dimension of derivations. Given a set of CHCs<jats:italic>P<\/jats:italic>, we define a transformation of<jats:italic>P<\/jats:italic>yielding a<jats:italic>dimension-bounded<\/jats:italic>set of CHCs<jats:italic>P<\/jats:italic><jats:sup>\u2264<jats:italic>k<\/jats:italic><\/jats:sup>. The set of derivations for<jats:italic>P<\/jats:italic><jats:sup>\u2264<jats:italic>k<\/jats:italic><\/jats:sup>consists of the derivations for<jats:italic>P<\/jats:italic>that have dimension at most<jats:italic>k<\/jats:italic>. We also show how to construct a set of clauses denoted<jats:italic>P<\/jats:italic><jats:sup>&gt;<jats:italic>k<\/jats:italic><\/jats:sup>whose derivations have dimension exceeding<jats:italic>k<\/jats:italic>. We then present algorithms using these constructions to decompose a CHC verification problem. One variation of this decomposition considers derivations of successively increasing dimension. The paper includes descriptions of implementations and experimental results.<\/jats:p>","DOI":"10.1017\/s1471068418000030","type":"journal-article","created":{"date-parts":[[2018,5,11]],"date-time":"2018-05-11T07:57:51Z","timestamp":1526025471000},"page":"224-251","source":"Crossref","is-referenced-by-count":4,"title":["Tree dimension in verification of constrained Horn clauses"],"prefix":"10.1017","volume":"18","author":[{"given":"BISHOKSAN","family":"KAFLE","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6984-7419","authenticated-orcid":false,"given":"JOHN P.","family":"GALLAGHER","sequence":"additional","affiliation":[]},{"given":"PIERRE","family":"GANTY","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2018,5,11]]},"reference":[{"key":"S1471068418000030_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8"},{"key":"S1471068418000030_ref33","doi-asserted-by":"crossref","unstructured":"Peralta J. , Gallagher J. P. and Sa\u011flam H. 1998. Analysis of imperative programs through analysis of constraint logic programs. In Proc. of International Static Analysis Symposium (SAS), G. Levi , Ed. Lecture Notes in Computer Science, vol. 1503. Springer-Verlag, 246\u2013261.","DOI":"10.1007\/3-540-49727-7_15"},{"volume-title":"Semantics with Applications \u2013 A Formal Introduction","year":"1992","author":"Nielson","key":"S1471068418000030_ref32"},{"key":"S1471068418000030_ref31","unstructured":"Mordvinov D. and Fedyukovich G. 2017. Synchronizing constrained horn clauses. In Proc. of 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21), T. Eiter and D. Sands , Eds. EPiC Series in Computing, vol. 46. EasyChair, 338\u2013355."},{"key":"S1471068418000030_ref35","unstructured":"R\u00fcmmer P. , Hojjat H. and Kuncak V. 2013. Disjunctive interpolants for Horn-clause verification. In Proc. of Computer-Aided Verification, N. Sharygina and H. Veith , Eds. Lecture Notes in Computer Science, vol 8044. Springer, 347\u2013363."},{"key":"S1471068418000030_ref29","doi-asserted-by":"crossref","unstructured":"Kafle B. , Gallagher J. P. and Morales J. F. 2016. RAHFT: A tool for verifying Horn clauses using abstract interpretation and finite tree automata. In Proc. of Computer-Aided Verification (CAV), S. Chaudhuri and A. Farzan , Eds. Lecture Notes in Computer Science, vol. 9779. Springer, 261\u2013268.","DOI":"10.1007\/978-3-319-41528-4_14"},{"volume-title":"Partial Evaluation and Automatic Software Generation","year":"1993","author":"Jones","key":"S1471068418000030_ref26"},{"key":"S1471068418000030_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10002-X"},{"key":"S1471068418000030_ref22","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000457"},{"key":"S1471068418000030_ref21","doi-asserted-by":"crossref","unstructured":"Heizmann M. , Hoenicke J. and Podelski A. 2013. Software model checking for people who love automata. In Proc. of Computer-Aided Verification, N. Sharygina and H. Veith , Eds. Lecture Notes in Computer Science, vol 8044. Springer, 36\u201352.","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"S1471068418000030_ref20","doi-asserted-by":"crossref","unstructured":"Heizmann M. , Hoenicke J. and Podelski A. 2009. Refinement of trace abstraction. In Proc. of International Static Analysis Symposium (SAS), J. Palsberg and Z. Su , Eds. Lecture Notes in Computer Science, vol. 5673. Springer, 69\u201385.","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"S1471068418000030_ref19","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/978-3-662-46681-0_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Gurfinkel","year":"2015"},{"key":"S1471068418000030_ref16","doi-asserted-by":"crossref","unstructured":"Gonnord L. and Halbwachs N. 2006. Combining widening and acceleration in linear relation analysis. In Proc. of International Static Analysis Symposium (SAS), K. Yi , Ed. Lecture Notes in Computer Science, vol. 4134. Springer, 144\u2013160.","DOI":"10.1007\/11823230_10"},{"key":"S1471068418000030_ref15","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1007\/s10009-016-0420-7","article-title":"Under-approximation of procedure summaries for integer programs","volume":"19","author":"Ganty","year":"2016","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"S1471068418000030_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61580-6_7"},{"key":"S1471068418000030_ref13","doi-asserted-by":"crossref","unstructured":"Gallagher J. P. 1993. Specialisation of logic programs: A tutorial. In Proc. of ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'93). ACM Press, Copenhagen, 88\u201398.","DOI":"10.1145\/154630.154640"},{"key":"S1471068418000030_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1857914.1857917"},{"key":"S1471068418000030_ref10","doi-asserted-by":"crossref","unstructured":"Esparza J. , Kiefer S. and Luttenberger M. 2007. On fixed point equations over commutative semirings. In Proc. of Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 4393. Springer, 296\u2013307.","DOI":"10.1007\/978-3-540-70918-3_26"},{"key":"S1471068418000030_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068415000289"},{"key":"S1471068418000030_ref7","doi-asserted-by":"crossref","unstructured":"De Angelis E. , Fioravanti F. , Pettorossi A. and Proietti M. 2014. Verimap: A tool for verifying programs through transformations. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems, E. \u00c1brah\u00e1m and K. Havelund , Eds. Lecture Notes in Computer Science, vol. 8413. Springer, 568\u2013574.","DOI":"10.1007\/978-3-642-54862-8_47"},{"key":"S1471068418000030_ref5","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II \u2013 Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday","author":"Bj\u00f8rner","year":"2015"},{"key":"S1471068418000030_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"S1471068418000030_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00730-2"},{"volume-title":"Structure and Interpretation of Computer Programs","year":"1996","author":"Abelson","key":"S1471068418000030_ref1"},{"key":"S1471068418000030_ref27","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.cl.2015.11.001","article-title":"Horn clause verification with convex polyhedral abstraction and tree automata-based refinement","volume":"47","author":"Kafle","year":"2017","journal-title":"Computer Languages, Systems and Structures"},{"key":"S1471068418000030_ref6","unstructured":"Bj\u00f8rner N. , McMillan K. L. and Rybalchenko A. 2013. On solving universally quantified Horn clauses. In Proc. of International Static Analysis Symposium (SAS), F. Logozzo and M. F\u00e4hndrich , Eds. Lecture Notes in Computer Science, vol. 7935. Springer, 105\u2013125."},{"key":"S1471068418000030_ref23","doi-asserted-by":"crossref","unstructured":"Hoder K. and Bj\u00f8rner N. 2012. Generalized property directed reachability. In Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT), A. Cimatti and R. Sebastiani , Eds. Lecture Notes in Computer Science, vol. 7317. Springer, 157\u2013171.","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"S1471068418000030_ref34","doi-asserted-by":"crossref","unstructured":"Reps T. W. , Turetsky E. and Prabhu P. 2016. Newtonian program analysis via tensor product. In Proc. of Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), R. Bod\u00edk and R. Majumdar , Eds. ACM, 663\u2013677.","DOI":"10.1145\/2837614.2837659"},{"key":"S1471068418000030_ref30","unstructured":"McMillan K. L. and Rybalchenko A. 2013. Solving constrained Horn clauses using interpolation. Technical Report MSR-TR-2013-6, Microsoft Research. https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/MSR-TR-2013-6.pdf"},{"key":"S1471068418000030_ref28","doi-asserted-by":"crossref","unstructured":"Kafle B. , Gallagher J. P. and Ganty P. 2016. Solving non-linear horn clauses using a linear horn clause solver. In Proc. of Workshop on Horn Clauses for Verification and Synthesis (HCVS), J. P. Gallagher and P. R\u00fcmmer , Eds. Electronic Proceedings in Theoretical Computer Science, vol. 219. 33\u201348.","DOI":"10.4204\/EPTCS.219.4"},{"key":"S1471068418000030_ref17","unstructured":"Grebenshchikov S. , Gupta A. , Lopes N. P. , Popeea C. and Rybalchenko A. 2012. HSF(C): A software verifier based on Horn clauses - (competition contribution). In Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), C. Flanagan and B. K\u00f6nig, Eds. Lecture Notes in Computer Science, vol. 7214. Springer, 549\u2013551."},{"key":"S1471068418000030_ref24","unstructured":"Hojjat H. , Konecn\u00fd F. , Garnier F. , Iosif R. , Kuncak V. and R\u00fcmmer P. 2012. A verification toolkit for numerical transition systems \u2013 Tool paper. In Proc. of International Symposium on Formal Methods (FM), D. Giannakopoulou and D. M\u00e9ry , Eds. Lecture Notes in Computer Science, vol. 7436. Springer, 247\u2013251."},{"key":"S1471068418000030_ref12","doi-asserted-by":"crossref","unstructured":"Esparza J. , Luttenberger M. and Schlund M. 2014. A brief history of strahler numbers. In Proc. of International Conference on Language and Automata Theory and Applications (LATA), A. H. Dediu , C. Mart\u00edn-Vide , J. L. Sierra-Rodr\u00edguez and B. Truthe , Eds. Lecture Notes in Computer Science, vol. 8370. Springer, 1\u201313.","DOI":"10.1007\/978-3-319-04921-2_1"},{"key":"S1471068418000030_ref4","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Beyer","year":"2015"},{"key":"S1471068418000030_ref18","doi-asserted-by":"crossref","unstructured":"Grebenshchikov S. , Lopes N. P. , Popeea C. and Rybalchenko A. 2012. Synthesizing software verifiers from proof rules. In Proc. of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), J. Vitek , H. Lin and F. Tip , Eds. ACM, 405\u2013416.","DOI":"10.1145\/2254064.2254112"},{"key":"S1471068418000030_ref9","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer-Aided Verification","author":"Dutertre","year":"2014"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068418000030","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,17]],"date-time":"2019-10-17T18:50:29Z","timestamp":1571338229000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068418000030\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,3]]}},"alternative-id":["S1471068418000030"],"URL":"https:\/\/doi.org\/10.1017\/s1471068418000030","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2018,3]]}}}