{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T00:31:29Z","timestamp":1768005089597,"version":"3.49.0"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415277","type":"print"},{"value":"9783319415284","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41528-4_14","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:06Z","timestamp":1468316046000},"page":"261-268","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata"],"prefix":"10.1007","author":[{"given":"Bishoksan","family":"Kafle","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John P.","family":"Gallagher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9 F.","family":"Morales","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"key":"14_CR1","unstructured":"SMT-LIB format. \n                      http:\/\/smtlib.cs.uiowa.edu\n                      \n                    . Accessed 5 May 2016"},{"issue":"1\u20132","key":"14_CR2","first-page":"3","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. SCP 72(1\u20132), 3\u201321 (2008)","journal-title":"SCP"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Bancilhon, F., Maier, D., Sagiv, Y., Ullman, J.: Magic sets and other strange ways to implement logic programs. In: Proceedings of the 5th ACM SIGMOD-SIGACT Symposium on Principles of Database Systems (1986)","DOI":"10.1145\/6012.15399"},{"key":"14_CR4","doi-asserted-by":"crossref","first-page":"594","DOI":"10.1007\/978-3-642-36742-7_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Dirk Beyer","year":"2013","unstructured":"Beyer, D.: Second competition on software verification - (summary of SV-COMP 2013). In: Piterman and Smolka [35], pp. 594\u2013609"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","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":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015)"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-38856-9_8","volume-title":"Static Analysis","author":"N Bj\u00f8rner","year":"2013","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified Horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 105\u2013125. Springer, Heidelberg (2013)"},{"issue":"4\u20135","key":"14_CR7","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s00165-008-0080-9","volume":"20","author":"AR Bradley","year":"2008","unstructured":"Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Asp. Comput. 20(4\u20135), 379\u2013405 (2008)","journal-title":"Formal Asp. Comput."},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/978-3-319-10431-7_20","volume-title":"Software Engineering and Formal Methods","author":"G Brat","year":"2014","unstructured":"Brat, G., Navas, J.A., Shi, N., Venet, A.: IKOS: a framework for static analysis based on abstract interpretation. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 271\u2013277. Springer, Heidelberg (2014)"},{"key":"14_CR9","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Alessandro Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman and Smolka [35], pp. 93\u2013107"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/3-540-36377-7_6","volume-title":"The Essence of Computation","author":"M Codish","year":"2002","unstructured":"Codish, M., S\u00f8ndergaard, H.: Meta-circular abstract interpretation in prolog. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 109\u2013134. Springer, Heidelberg (2002)"},{"key":"14_CR11","doi-asserted-by":"crossref","first-page":"325","DOI":"10.4204\/EPTCS.129.19","volume":"129","author":"Agostino Cortesi","year":"2013","unstructured":"Cortesi, A., Costantini, G., Ferrara, P.: A survey on product operators in abstract interpretation. In: Banerjee, A., Danvy, O., Doh, K., Hatcliff, J. (eds.) Semantics, Abstract Interpretation, and Reasoning About Programs. EPTCS, vol. 129, pp. 325\u2013336 (2013)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"14_CR12","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":"14_CR13","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":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-642-19805-2_31","volume-title":"Foundations of Software Science and Computational Structures","author":"P Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Mauborgne, L.: The reduced product of abstract domains and the combination of decision procedures. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 456\u2013472. Springer, Heidelberg (2011)"},{"key":"14_CR15","first-page":"149","volume":"95","author":"E De Angelis","year":"2014","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Program verification via iterated specialization. SCP 95, 149\u2013175 (2014)","journal-title":"SCP"},{"key":"14_CR16","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 De Angelis","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. 8413, pp. 568\u2013574. Springer, Heidelberg (2014)"},{"key":"14_CR17","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/0743-1066(94)90050-7","volume":"18","author":"S Debray","year":"1994","unstructured":"Debray, S., Ramakrishnan, R.: Abstract interpretation of logic programs using magic transformations. J. Logic Program. 18, 149\u2013176 (1994)","journal-title":"J. Logic Program."},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Heidelberg (2014)"},{"key":"14_CR19","unstructured":"Gallagher, J.P., Ajspur, M., Kafle, B.: An optimised algorithm for determinisation and completion of finite tree automata. CoRR, abs\/1511.03595 (2015)"},{"key":"14_CR20","unstructured":"Gallagher, J.P., Kafle, B.: Analysis and transformation tools for constrained Horn clause verification. TPLP 14(4\u20135 (additional materials in online edition)), 90\u2013101 (2014)"},{"issue":"6","key":"14_CR21","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1145\/2345156.2254112","volume":"47","author":"Sergey Grebenshchikov","year":"2012","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Vitek, J., Lin, H., Tip, F. (eds.) PLDI, pp. 405\u2013416. ACM (2012)","journal-title":"ACM SIGPLAN Notices"},{"key":"14_CR22","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":"BS 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. 4963, pp. 443\u2013458. Springer, Heidelberg (2008)"},{"key":"14_CR23","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. 5643, pp. 634\u2013640. Springer, Heidelberg (2009)"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Heidelberg (2015)"},{"key":"14_CR25","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. 5673, pp. 69\u201385. Springer, Heidelberg (2009)"},{"issue":"1\u20132","key":"14_CR26","first-page":"219","volume":"12","author":"MV Hermenegildo","year":"2012","unstructured":"Hermenegildo, M.V., Bueno, F., Carro, M., L\u00f3pez-Garc\u00eda, P., Mera, E., Morales, J.F., Puebla, G.: An overview of Ciao and its design philosophy. TPLP 12(1\u20132), 219\u2013252 (2012)","journal-title":"TPLP"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-32759-9_21","volume-title":"FM 2012: Formal Methods","author":"H Hojjat","year":"2012","unstructured":"Hojjat, H., Kone\u010dn\u00fd, F., Garnier, F., Iosif, R., Kuncak, V., R\u00fcmmer, P.: A verification toolkit for numerical transition systems - tool paper. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 247\u2013251. Springer, Heidelberg (2012)"},{"key":"14_CR28","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"1920","author":"J Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.: Constraint logic programming: a survey. J. Logic Program. 1920, 503\u2013581 (1994)","journal-title":"J. Logic Program."},{"key":"14_CR29","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. 7358, pp. 758\u2013766. Springer, Heidelberg (2012)"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Kafle, B., Gallagher, J.P.: Constraint specialisation in Horn clause verification. In: Asai, K., Sagonas, K. (eds.) Proceedings Workshop on PEPM, PEPM, Mumbai, India, 15\u201317 January 2015, pp. 85\u201390. ACM (2015)","DOI":"10.1145\/2678015.2682544"},{"key":"14_CR31","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.cl.2015.11.001","volume":"47","author":"Bishoksan Kafle","year":"2017","unstructured":"Kafle, B., Gallagher, J.P.: Horn clause verification with convex polyhedral abstraction and tree automata-based refinement. Comput. Lang. Syst. Struct. (2015, In press). \n                      http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1477842415000822\n                      \n                    , doi:\n                      10.1016\/j.cl.2015.11.001","journal-title":"Computer Languages, Systems & Structures"},{"key":"14_CR32","doi-asserted-by":"crossref","unstructured":"Kafle, B., Gallagher, J.P.: Interpolant tree automata and their application in Horn clause verification. CoRR, abs\/1601.06521 (2016)","DOI":"10.4204\/EPTCS.216.6"},{"key":"14_CR33","unstructured":"McMillan, K.L.: Interpolants from Z3 proofs. In: Bjesse, P., Slobodov\u00e1, A. (eds.) FMCAD 2011, Austin, TX, USA, 30 October\u201302 November 2011, pp. 19\u201327. FMCAD Inc. (2011)"},{"key":"14_CR34","unstructured":"McMillan, K.L., Rybalchenko, A.: Solving constrained Horn clauses using interpolation. Technical report, Microsoft Research (2013)"},{"key":"14_CR35","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","year":"2013","unstructured":"Piterman, N., Smolka, S.A. (eds.): TACAS 2013 (ETAPS 2013). LNCS, vol. 7795. Springer, Heidelberg (2013)"},{"issue":"11","key":"14_CR36","doi-asserted-by":"publisher","first-page":"1212","DOI":"10.1016\/j.jsc.2010.06.005","volume":"45","author":"A Rybalchenko","year":"2010","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. J. Symb. Comput. 45(11), 1212\u20131233 (2010)","journal-title":"J. Symb. Comput."},{"key":"14_CR37","unstructured":"Wang, W., Jiao, L.: Trace abstraction refinement for solving Horn clauses. Technical report ISCAS-SKLCS-15-19, SCAS-SKLCS, December 2015. \n                      http:\/\/lcs.ios.ac.cn\/wangwf\/TechReportISCAS-SKLCS-15-19.pdf"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41528-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:04:39Z","timestamp":1594685079000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41528-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415277","9783319415284"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41528-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}