{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T11:20:40Z","timestamp":1740136840697,"version":"3.37.3"},"reference-count":44,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Computer Languages, Systems & Structures"],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1016\/j.cl.2015.11.001","type":"journal-article","created":{"date-parts":[[2015,11,13]],"date-time":"2015-11-13T01:35:10Z","timestamp":1447378510000},"page":"2-18","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":9,"special_numbering":"P1","title":["Horn clause verification with convex polyhedral abstraction and tree automata-based refinement"],"prefix":"10.1016","volume":"47","author":[{"given":"Bishoksan","family":"Kafle","sequence":"first","affiliation":[]},{"given":"John P.","family":"Gallagher","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.cl.2015.11.001_bib1","doi-asserted-by":"crossref","unstructured":"Peralta J, Gallagher JP, Sa\u011flam H. Analysis of imperative programs through analysis of constraint logic programs. In: Levi G, editor, Static analysis. 5th international symposium, SAS\u05f398, Pisa. Lecture notes in computer science, vol. 1503. Springer-Verlag; 1998. p. 246\u201361.","DOI":"10.1007\/3-540-49727-7_15"},{"key":"10.1016\/j.cl.2015.11.001_bib2","doi-asserted-by":"crossref","unstructured":"Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A. Synthesizing software verifiers from proof rules. In: Vitek J, Lin H, Tip F, editors, ACM SIGPLAN conference on programming language design and implementation, PLDI \u05f312, Beijing, China, June 11\u201316, 2012. ACM; 2012. p. 405\u201316. http:\/\/dx.doi.org\/10.1145\/2254064.2254112. URL: \u3008http:\/\/doi.acm.org\/10.1145\/2254064.2254112\u3009","DOI":"10.1145\/2254064.2254112"},{"issue":"3","key":"10.1016\/j.cl.2015.11.001_bib3","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/s100090100049","article-title":"Constraint-based deductive model checking","volume":"3","author":"Delzanno","year":"2001","journal-title":"STTT"},{"key":"10.1016\/j.cl.2015.11.001_bib4","doi-asserted-by":"crossref","unstructured":"Jaffar J, Santosa AE, Voicu R. Modeling systems in CLP. In: Gabbrielli M, Gupta G, editors, Logic programming, 21st international conference, ICLP 2005, Sitges, Spain. Proceedings. Lecture notes in computer science, vol. 3668. Springer, October 2\u20135, 2005. p. 412\u20133. http:\/\/dx.doi.org\/10.1007\/11562931_34. URL \u3008http:\/\/dx.doi.org\/10.1007\/11562931_34\u3009","DOI":"10.1007\/11562931_34"},{"key":"10.1016\/j.cl.2015.11.001_bib5","doi-asserted-by":"crossref","unstructured":"Gurfinkel A, Kahsai T, Komuravelli A, Navas JA. The seahorn verification framework, in: D. Kroening, CS. Pasareanu (Eds.), Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Vol. 9206 of Lecture Notes in Computer Science, Springer, 2015, pp. 343\u2013361. http:\/\/dx.doi.org\/10.1007\/978-3-319-21690-4_20.","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"10.1016\/j.cl.2015.11.001_bib6","doi-asserted-by":"crossref","unstructured":"De Angelis E, Fioravanti F, Pettorossi A, Proietti M. Semantics-based generation of verification conditions by program specialization. In: Falaschi M, Albert E, editors, Proceedings of the 17th international symposium on principles and practice of declarative programming, Siena, Italy. ACM; July 14\u201316, 2015. p. 91\u2013102. http:\/\/dx.doi.org\/10.1145\/2790449.2790529. URL \u3008http:\/\/doi.acm.org\/10.1145\/2790449.2790529\u3009.","DOI":"10.1145\/2790449.2790529"},{"key":"10.1016\/j.cl.2015.11.001_bib7","doi-asserted-by":"crossref","unstructured":"Heizmann M, Hoenicke J, Podelski A. Refinement of trace abstraction. In: Palsberg J, Su Z, editors, Static analysis. 16th international symposium. SAS 2009, Los Angeles, CA, USA. Lecture notes in computer science, vol. 5673. Springer; 2009. p. 69\u201385. http:\/\/dx.doi.org\/10.1007\/978-3-642-03237-0_7. URL \u3008http:\/\/dx.doi.org\/10.1007\/978-3-642-03237-0_7\u3009.","DOI":"10.1007\/978-3-642-03237-0_7"},{"issue":"5","key":"10.1016\/j.cl.2015.11.001_bib8","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","article-title":"Counterexample-guided abstraction refinement for symbolic model checking","volume":"50","author":"Clarke","year":"2003","journal-title":"J ACM"},{"key":"10.1016\/j.cl.2015.11.001_bib9","doi-asserted-by":"crossref","unstructured":"Kafle B, Gallagher JP. Tree automata-based refinement with application to horn clause verification. In: D\u05f3Souza D, Lal A, Larsen KG, editors, Verification, model checking, and abstract interpretation\u201416th international conference, VMCAI 2015, Mumbai, India, January 12\u201314, 2015. Proceedings, Lecture notes in computer science, vol. 8931. Springer; 2015. p. 209\u201326. http:\/\/dx.doi.org\/10.1007\/978-3-662-46081-8_12. URL: \u3008http:\/\/dx.doi.org\/10.1007\/978-3-662-46081-8_12\u3009","DOI":"10.1007\/978-3-662-46081-8_12"},{"key":"10.1016\/j.cl.2015.11.001_bib10","unstructured":"Comon H, Dauchet M, Gilleron R, L\u00f6ding C, Jacquemard F, Lugiez D, et al. Tree automata techniques and applications. Available on: \u3008http:\/\/www.grappa.univ-lille3.fr\/tata\u3009, release October 12, 2007; 2007."},{"key":"10.1016\/j.cl.2015.11.001_bib11","unstructured":"Gallagher JP, Ajspur M, Kafle B. An optimised algorithm for determinisation and completion of finite tree automata. Technical report 145. Roskilde University, Denmark. Available from \u3008http:\/\/akira.ruc.dk\/~jpg\/dfta.pdf\u3009; September 2014."},{"key":"10.1016\/j.cl.2015.11.001_bib12","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","article-title":"Constraint logic programming","volume":"19\/20","author":"Jaffar","year":"1994","journal-title":"J Logic Progr"},{"key":"10.1016\/j.cl.2015.11.001_bib13","doi-asserted-by":"crossref","unstructured":"Jaffar J, Maher M. Constraint logic programming: a survey. In: Gabbay DM, Hogger C, Robinson J, editors, Handbook of logic in artificial intelligence and logic programming: logic programming, vol. 5. Oxford, United Kingdom: Oxford University Press; 1998. p. 591\u2013696.","DOI":"10.1093\/oso\/9780198537922.003.0012"},{"key":"10.1016\/j.cl.2015.11.001_bib14","unstructured":"St\u00e4rk RF. A direct proof for the completeness of SLD-resolution. In: B\u00f6rger E, B\u00fcning HK, Richter MM, editors, CSL \u05f389, 3rd workshop on computer science logic, Kaiserslautern, Germany, October 2\u20136, 1989. Proceedings. Lecture notes in computer science, vol. 440. Springer; 1989. p. 382\u20133."},{"key":"10.1016\/j.cl.2015.11.001_bib15","doi-asserted-by":"crossref","unstructured":"Gallagher JP, Lafave L. Regular approximation of computation paths in logic and functional languages. In: Danvy O, Gl\u00fcck R, Thiemann R, editors, Partial evaluation. Saarland, Germany: Lecture notes in computer science, vol. 1110. Springer-Verlag; 1996. p. 115\u201336.","DOI":"10.1007\/3-540-61580-6_7"},{"key":"10.1016\/j.cl.2015.11.001_bib16","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham RM, Harrison MA, Sethi R, editors, POPL. Los Angeles, CA, USA: ACM; 1977. p. 238\u201352.","DOI":"10.1145\/512950.512973"},{"key":"10.1016\/j.cl.2015.11.001_bib17","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N. Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th annual ACM symposium on principles of programming languages; 1978. p. 84\u201396.","DOI":"10.1145\/512760.512770"},{"key":"10.1016\/j.cl.2015.11.001_bib18","doi-asserted-by":"crossref","unstructured":"Benoy F, King A. Inferring argument size relationships with CLP(R). In: Gallagher JP, editor, Logic-based program synthesis and transformation (LOPSTR\u05f396). Lecture notes in computer science, vol. 1207; 1996. p. 204\u201323.","DOI":"10.1007\/3-540-62718-9_12"},{"key":"10.1016\/j.cl.2015.11.001_bib19","doi-asserted-by":"crossref","unstructured":"Halbwachs N, Proy YE, Raymound P. Verification of linear hybrid systems by means of convex approximations. In: Proceedings of the first symposium on static analysis. Lecture notes in computer science, vol. 864; 1994. p. 223\u201337.","DOI":"10.1007\/3-540-58485-4_43"},{"issue":"1\u20132","key":"10.1016\/j.cl.2015.11.001_bib20","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","article-title":"The Parma Polyhedra Library","volume":"72","author":"Bagnara","year":"2008","journal-title":"Sci Comput Progr"},{"key":"10.1016\/j.cl.2015.11.001_bib21","doi-asserted-by":"crossref","unstructured":"Lakhdar-Chaouch L, Jeannet B, Girault A. Widening with thresholds for programs with complex control graphs. In: Bultan T, Hsiung P-A, editors, ATVA 2011, Taipei, Taiwan. Lecture notes in computer science, vol. 6996. Springer; 2011. p. 492\u2013502.","DOI":"10.1007\/978-3-642-24372-1_38"},{"key":"10.1016\/j.cl.2015.11.001_bib22","doi-asserted-by":"crossref","unstructured":"Kafle B, Gallagher JP. Constraint specialisation in horn clause verification. In: Asai K, Sagonas K, editors, Proceedings of the 2015 workshop on partial evaluation and program manipulation, PEPM, Mumbai, India, January 15\u201317, 2015. ACM; 2015. p. 85\u201390. http:\/\/dx.doi.org\/10.1145\/2678015.2682544. URL: \u3008http:\/\/doi.acm.org\/10.1145\/2678015.2682544\u3009.","DOI":"10.1145\/2678015.2682544"},{"key":"10.1016\/j.cl.2015.11.001_bib23","unstructured":"Gallagher JP, Kafle B. Analysis and transformation tools for constrained Horn clause verification, TPLP 14 (4\u20135 (additional materials in online edition)); 2014. p. 90\u2013101. URL: \u3008http:\/\/journals.cambridge.org\/action\/displaySuppMaterial?cupCode=1&type=4&jid=TLP&volumeId=14&issueId=4-5&aid=9303163\u3009."},{"key":"10.1016\/j.cl.2015.11.001_bib24","doi-asserted-by":"crossref","unstructured":"Gulavani BS, Chakraborty S, Nori AV, Rajamani SK. Automatically refining abstract interpretations. In: Ramakrishnan CR, Rehof J, editors, TACAS. Budapest, Hungary. Lecture notes in computer science, vol. 4963. Springer; 2008. p. 443\u201358.","DOI":"10.1007\/978-3-540-78800-3_33"},{"key":"10.1016\/j.cl.2015.11.001_bib25","doi-asserted-by":"crossref","unstructured":"Jaffar J, Murali V, Navas JA, Santosa AE. Tracer: a symbolic execution tool for verification. In: Madhusudan P, Seshia SA, editors, CAV. Berkeley, CA, USA: Lecture notes in computer science, vol. 7358. Springer; 2012. p. 758\u201366.","DOI":"10.1007\/978-3-642-31424-7_61"},{"key":"10.1016\/j.cl.2015.11.001_bib26","doi-asserted-by":"crossref","unstructured":"Gupta A, Rybalchenko A. Invgen: an efficient invariant generator. In: Bouajjani A, Maler O, editors, CAV. Grenoble, France: Lecture notes in computer science, vol. 5643. Springer; 2009. p. 634\u201340.","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"10.1016\/j.cl.2015.11.001_bib27","doi-asserted-by":"crossref","unstructured":"Beyer D. Second competition on software verification\u2014(summary of sv-comp 2013). In: Piterman N, Smolka SA, editors, TACAS. Rome, Italy: Lecture notes in computer science, vol. 7795. Springer; 2013. p. 594\u2013609.","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"10.1016\/j.cl.2015.11.001_bib28","doi-asserted-by":"crossref","unstructured":"Podelski A, Rybalchenko A. ARMC: the logical choice for software model checking with abstraction refinement. In: Hanus M, editor, PADL 2007. Lecture notes in computer science, vol. 4354; 2007. p. 245\u201359.","DOI":"10.1007\/978-3-540-69611-7_16"},{"key":"10.1016\/j.cl.2015.11.001_bib29","doi-asserted-by":"crossref","unstructured":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. Hsf(c): a software verifier based on Horn clauses\u2014(competition contribution). In: Flanagan C, K\u00f6nig B, editors, TACAS. Tallinn, Estonia: Lecture notes in computer science, vol. 7214. Springer; 2012. p. 549\u201351.","DOI":"10.1007\/978-3-642-28756-5_46"},{"key":"10.1016\/j.cl.2015.11.001_bib30","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/j.scico.2014.05.017","article-title":"Program verification via iterated specialization","volume":"95","author":"De Angelis","year":"2014","journal-title":"Sci Comput Progr"},{"key":"10.1016\/j.cl.2015.11.001_bib31","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer P, Hojjat H, Kuncak V. Disjunctive interpolants for horn-clause verification. In: Sharygina N, Veith H, editors, CAV 2013. Proceedings. Saint Petersburg, Russia: Lecture notes in computer science, vol. 8044. Springer; 2013. p. 347\u201363.","DOI":"10.1007\/978-3-642-39799-8_24"},{"key":"10.1016\/j.cl.2015.11.001_bib32","doi-asserted-by":"crossref","unstructured":"Beyer D. Software verification and verifiable witnesses\u2014(report on SV-COMP 2015). In: Baier C, Tinelli C, editors, Tools and algorithms for the construction and analysis of systems\u201421st international conference, TACAS 2015. Held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11\u201318, 2015. Proceedings. Lecture notes in computer science, vol. 9035. Springer; 2015. p. 401\u201316. http:\/\/dx.doi.org\/10.1007\/978-3-662-46681-0. URL: \u3008http:\/\/dx.doi.org\/10.1007\/978-3-662-46681-0\u3009. http:\/\/dx.doi.org\/10.1007\/978-3-662-46681-0_31. URL: \u3008http:\/\/dx.doi.org\/10.1007\/978-3-662-46681-0_31\u3009.","DOI":"10.1007\/978-3-662-46681-0_31"},{"key":"10.1016\/j.cl.2015.11.001_bib33","doi-asserted-by":"crossref","unstructured":"Gurfinkel A, Kahsai T, Navas JA. Seahorn: a framework for verifying C programs (competition contribution). In: Baier C, Tinelli C, editors, Tools and algorithms for the construction and analysis of systems\u201421st international conference, TACAS 2015. Held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11\u201318, 2015. Proceedings. Lecture notes in computer science, vol. 9035. Springer; 2015. p. 447\u2013450. http:\/\/dx.doi.org\/10.1007\/978-3-662-46681-0. URL: \u3008http:\/\/dx.doi.org\/10.1007\/978-3-662-46681-0\u3009. http:\/\/dx.doi.org\/10.1007\/978-3-662-46681-0_41. URL: \u3008http:\/\/dx.doi.org\/10.1007\/978-3-662-46681-0_41\u3009.","DOI":"10.1007\/978-3-662-46681-0"},{"key":"10.1016\/j.cl.2015.11.001_bib34","doi-asserted-by":"crossref","unstructured":"Heizmann M, Hoenicke J, Podelski A. Nested interpolants. In: Hermenegildo MV, Palsberg J, editors, Proceedings of POPL 2010. Madrid, Spain: ACM; 2010. p. 471\u201382.","DOI":"10.1145\/1706299.1706353"},{"key":"10.1016\/j.cl.2015.11.001_bib35","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/S1571-0661(05)80052-0","article-title":"Abstract interpretation based verification of logic programs","volume":"40","author":"Levi","year":"2000","journal-title":"Electr Notes Theor Comput Sci"},{"key":"10.1016\/j.cl.2015.11.001_bib36","doi-asserted-by":"crossref","unstructured":"De Angelis E, Fioravanti F, Pettorossi A, Proietti M. Verifying programs via iterated specialization. In: Albert E, Mu S-C, editors, PEPM. Rome, Italy: ACM; 2013. p. 43\u201352.","DOI":"10.1145\/2426890.2426899"},{"key":"10.1016\/j.cl.2015.11.001_bib37","doi-asserted-by":"crossref","unstructured":"De Angelis E, Fioravanti F, Pettorossi A, Proietti M. Verimap: a tool for verifying programs through transformations. In: \u00c1brah\u00e1m E, Havelund K, editors, TACAS. Grenoble, France: Lecture notes in computer science, vol. 8413. Springer; 2014. p. 568\u201374.","DOI":"10.1007\/978-3-642-54862-8_47"},{"key":"10.1016\/j.cl.2015.11.001_bib38","unstructured":"Burke M, Soffa ML, editors, Proceedings of the 2001 ACM SIGPLAN conference on programming language design and implementation (PLDI), Snowbird, Utah, USA, June 20\u201322, 2001. ACM; 2001."},{"key":"10.1016\/j.cl.2015.11.001_bib39","unstructured":"Launchbury J, Mitchell JC, editors, Conference record of POPL 2002: the 29th SIGPLAN-SIGACT symposium on principles of programming languages, Portland, OR, USA, January 16\u201318, 2002. ACM; 2002."},{"key":"10.1016\/j.cl.2015.11.001_bib40","doi-asserted-by":"crossref","unstructured":"Albarghouthi A, Gurfinkel A, Chechik M. Craig interpretation. In: Min\u00e9 A, Schmidt D, editors, SAS. Deauville, France: Lecture notes in computer science, vol. 7460. Springer; 2012. p. 300\u201316.","DOI":"10.1007\/978-3-642-33125-1_21"},{"key":"10.1016\/j.cl.2015.11.001_bib41","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner N, McMillan KL, Rybalchenko A. On solving universally quantified Horn clauses. In: Logozzo F, F\u00e4hndrich M, editors, SAS. Seattle, Washington, USA. Lecture notes in computer science, vol. 7935. Springer; 2013. p. 105\u201325.","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"10.1016\/j.cl.2015.11.001_bib42","doi-asserted-by":"crossref","unstructured":"Gupta A, Popeea C, Rybalchenko A. Solving recursion-free Horn clauses over li+uif. In: Yang H, editor, APLAS. Kenting, Taiwan: Lecture notes in computer science, vol. 7078. Springer; 2011. p. 188\u2013203.","DOI":"10.1007\/978-3-642-25318-8_16"},{"issue":"7","key":"10.1016\/j.cl.2015.11.001_bib43","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/1965724.1965743","article-title":"A decade of software model checking with SLAM","volume":"54","author":"Ball","year":"2011","journal-title":"Commun ACM"},{"issue":"4\u20135","key":"10.1016\/j.cl.2015.11.001_bib44","first-page":"593","article-title":"Failure tabled constraint logic programming by interpolation","volume":"13","author":"Gange","year":"2013","journal-title":"TPLP"}],"container-title":["Computer Languages, Systems & Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1477842415000822?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1477842415000822?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2022,5,26]],"date-time":"2022-05-26T01:23:18Z","timestamp":1653528198000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1477842415000822"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":44,"alternative-id":["S1477842415000822"],"URL":"https:\/\/doi.org\/10.1016\/j.cl.2015.11.001","relation":{},"ISSN":["1477-8424"],"issn-type":[{"type":"print","value":"1477-8424"}],"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Horn clause verification with convex polyhedral abstraction and tree automata-based refinement","name":"articletitle","label":"Article Title"},{"value":"Computer Languages, Systems & Structures","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.cl.2015.11.001","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2015 Elsevier Ltd. All rights reserved.","name":"copyright","label":"Copyright"}]}}