{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T09:07:42Z","timestamp":1762506462234},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662460801"},{"type":"electronic","value":"9783662460818"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46081-8_12","type":"book-chapter","created":{"date-parts":[[2014,12,11]],"date-time":"2014-12-11T04:25:44Z","timestamp":1418271944000},"page":"209-226","source":"Crossref","is-referenced-by-count":8,"title":["Tree Automata-Based Refinement with Application to Horn Clause Verification"],"prefix":"10.1007","author":[{"given":"Bishoksan","family":"Kafle","sequence":"first","affiliation":[]},{"given":"John P.","family":"Gallagher","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_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)"},{"issue":"1\u20132","key":"12_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R. Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming\u00a072(1\u20132), 3\u201321 (2008)","journal-title":"Science of Computer Programming"},{"issue":"7","key":"12_CR3","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T. Ball","year":"2011","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM\u00a054(7), 68\u201376 (2011)","journal-title":"Commun. ACM"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/3-540-62718-9_12","volume-title":"Logic Program Synthesis and Transformation","author":"F. Benoy","year":"1997","unstructured":"Benoy, F., King, A.: Inferring argument size relationships with CLP(\n                  \n                    \n                  \n                  $\\mathcal{R}$\n                ). In: Gallagher, J. (ed.) LOPSTR 1996. LNCS, vol.\u00a01207, pp. 204\u2013223. Springer, Heidelberg (1997)"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Second competition on software verification - (summary of SV-COMP 2013). In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 594\u2013609. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified Horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol.\u00a07935, pp. 105\u2013125. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"12_CR7","unstructured":"Burke, M., Soffa, M.L. (eds.): Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird, Utah, USA, June 20-22. ACM (2001)"},{"issue":"5","key":"12_CR8","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"12_CR9","unstructured":"Comon, H., Dauchet, M., Gilleron, R., L\u00f6ding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007), \n                  \n                    http:\/\/www.grappa.univ-lille3.fr\/tata\n                  \n                  \n                 (release October 12, 2007)"},{"key":"12_CR10","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, R.M., Harrison, M.A., Sethi, R. (eds.) POPL, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"12_CR11","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, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"12_CR12","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. (eds.) PEPM, pp. 43\u201352. ACM (2013)","DOI":"10.1145\/2426890.2426899"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/978-3-642-54862-8_47","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Angelis De","year":"2014","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: VeriMAP: A tool for verifying programs through transformations. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol.\u00a08413, pp. 568\u2013574. Springer, Heidelberg (2014)"},{"key":"12_CR14","unstructured":"Gallagher, J.P., Ajspur, M., Kafle, B.: An Optimised Algorithm for Determinisation and Completion of Finite Tree Automata. Technical Report 145, Roskilde University, Denmark, (September 2014), \n                  \n                    http:\/\/akira.ruc.dk\/~jpg\/dfta.pdf"},{"key":"12_CR15","unstructured":"Gallagher, J.P., Kafle, B.: Analysis and transformation tools for constrained Horn clause verification. TPLP, 14(4-5) (additional materials in online edition), 90\u2013101 (2014)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/3-540-61580-6_7","volume-title":"Partial Evaluation","author":"J.P. Gallagher","year":"1996","unstructured":"Gallagher, J.P., Lafave, L.: Regular approximation of computation paths in logic and functional languages. In: Danvy, O., Thiemann, P., Gl\u00fcck, R. (eds.) Dagstuhl Seminar 1996. LNCS, vol.\u00a01110, pp. 115\u2013136. Springer, Heidelberg (1996)"},{"issue":"4-5","key":"12_CR17","first-page":"593","volume":"13","author":"G. Gange","year":"2013","unstructured":"Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Failure tabled constraint logic programming by interpolation. TPLP\u00a013(4-5), 593\u2013607 (2013)","journal-title":"TPLP"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1007\/978-3-642-28756-5_46","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Grebenshchikov","year":"2012","unstructured":"Grebenshchikov, S., Gupta, A., Lopes, N.P., Popeea, C., Rybalchenko, A.: HSF(C): A software verifier based on Horn clauses - (competition contribution). In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 549\u2013551. Springer, Heidelberg (2012)"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-78800-3_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B.S. Gulavani","year":"2008","unstructured":"Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 443\u2013458. Springer, Heidelberg (2008)"},{"key":"12_CR20","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":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/978-3-642-02658-4_48","volume-title":"Computer Aided Verification","author":"A. Gupta","year":"2009","unstructured":"Gupta, A., Rybalchenko, A.: InvGen: An efficient invariant generator. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 634\u2013640. Springer, Heidelberg (2009)"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-58485-4_43","volume-title":"Static Analysis","author":"N. Halbwachs","year":"1994","unstructured":"Halbwachs, N., Proy, Y.E., Raymound, P.: Verification of linear hybrid systems by means of convex approximations. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol.\u00a0864, pp. 223\u2013237. Springer, Heidelberg (1994)"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-03237-0_7","volume-title":"Static Analysis","author":"M. Heizmann","year":"2009","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 69\u201385. Springer, Heidelberg (2009)"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of POPL 2010, pp. 471\u2013482. ACM (2010)","DOI":"10.1145\/1707801.1706353"},{"key":"12_CR25","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19\/20","author":"J. Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.: Constraint Logic Programming: A Survey. Journal of Logic Programming\u00a019\/20, 503\u2013581 (1994)","journal-title":"Journal of Logic Programming"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1007\/978-3-642-31424-7_61","volume-title":"Computer Aided Verification","author":"J. Jaffar","year":"2012","unstructured":"Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: TRACER: A symbolic execution tool for verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 758\u2013766. Springer, Heidelberg (2012)"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-24372-1_38","volume-title":"Automated Technology for Verification and Analysis","author":"L. Lakhdar-Chaouch","year":"2011","unstructured":"Lakhdar-Chaouch, L., Jeannet, B., Girault, A.: Widening with thresholds for programs with complex control graphs. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 492\u2013502. Springer, Heidelberg (2011)"},{"key":"12_CR28","unstructured":"Launchbury, J., Mitchell, J.C. (eds.): Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18. ACM (2002)"},{"key":"12_CR29","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S1571-0661(05)80052-0","volume":"40","author":"G. Levi","year":"2000","unstructured":"Levi, G.: Abstract interpretation based verification of logic programs. Electr. Notes Theor. Comput. Sci.\u00a040, 243 (2000)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"12_CR30","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":"12_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A. Podelski","year":"2007","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 245\u2013259. Springer, Heidelberg (2007)"},{"key":"12_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-642-39799-8_24","volume-title":"Computer Aided Verification","author":"P. R\u00fcmmer","year":"2013","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 347\u2013363. Springer, Heidelberg (2013)"},{"key":"12_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/3-540-52753-2_52","volume-title":"CSL \u201989","author":"R.F. St\u00e4rk","year":"1990","unstructured":"St\u00e4rk, R.F.: A direct proof for the completeness of SLD-resolution. In: B\u00f6rger, E., Kleine B\u00fcning, H., Richter, M.M. (eds.) CSL 1989. LNCS, vol.\u00a0440, pp. 382\u2013383. Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46081-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T20:35:41Z","timestamp":1559075741000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46081-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662460801","9783662460818"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46081-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}