Tree automata-based refinement with application to Horn clause verification

Bishoksan Kafle, John Patrick Gallagher

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

In this paper we apply tree-automata techniques to refinement of abstract interpretation in Horn clause verification.
We go beyond previous work on refining trace abstractions; firstly we handle tree automata rather than string automata and thereby can capture traces in any Horn clause derivations rather than just transition systems; secondly, we show how algorithms manipulating tree automata interact with abstract interpretations, establishing progress in refinement and generating refined clauses that eliminate causes of imprecision.
We show how to derive a refined set of Horn clauses in which given infeasible traces have been eliminated, using a recent optimised algorithm for tree automata determinisation. We also show how we can introduce disjunctive abstractions selectively by splitting states in the tree automaton. The approach is independent of the abstract domain and constraint theory underlying the Horn clauses. Experiments using linear constraint problems and the abstract domain of convex polyhedra show that the refinement technique is practical and that iteration of abstract interpretation with tree automata-based refinement solves many challenging Horn clause verification problems. We compare the results with other state of the art Horn clause verification tools.
Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation
EditorsDeepak D'Souza, Akash Lal, Kim Guldstrand Larsen
Number of pages18
Volume8931
PublisherSpringer
Publication date2015
Pages209-226
ISBN (Print)978-3-662-46080-1
DOIs
Publication statusPublished - 2015
Event16th International Conference on Verification, Model Checking, and Abstract Interpretation - Mumbai, India
Duration: 12 Jan 201514 Jan 2015
http://research.microsoft.com/en-us/events/vmcai2015/

Conference

Conference16th International Conference on Verification, Model Checking, and Abstract Interpretation
CountryIndia
CityMumbai
Period12/01/201514/01/2015
Internet address
SeriesLecture Notes in Computer Science
Number8931
ISSN0302-9743

Bibliographical note

@inproceedings{DBLP:conf/vmcai/KafleG15,
author = {Bishoksan Kafle and
John P. Gallagher},
title = {Tree Automata-Based Refinement with Application to Horn Clause Verification},
booktitle = {Verification, Model Checking, and Abstract Interpretation - 16th International
Conference, {VMCAI} 2015, Mumbai, India, January 12-14, 2015. Proceedings},
pages = {209--226},
year = {2015},
crossref = {DBLP:conf/vmcai/2015},
url = {http://dx.doi.org/10.1007/978-3-662-46081-8_12},
doi = {10.1007/978-3-662-46081-8_12},
timestamp = {Fri, 12 Dec 2014 12:30:11 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/KafleG15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/vmcai/2015,
editor = {Deepak D'Souza and
Akash Lal and
Kim Guldstrand Larsen},
title = {Verification, Model Checking, and Abstract Interpretation - 16th International
Conference, {VMCAI} 2015, Mumbai, India, January 12-14, 2015. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8931},
publisher = {Springer},
year = {2014},
url = {http://dx.doi.org/10.1007/978-3-662-46081-8},
doi = {10.1007/978-3-662-46081-8},
isbn = {978-3-662-46080-1},
timestamp = {Fri, 12 Dec 2014 12:27:22 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/2015},
bibsource = {dblp computer science bibliography, http://dblp.org}
}

Keywords

  • finite tree automata
  • Abstract Interpretation
  • Horn clauses

Cite this

Kafle, B., & Gallagher, J. P. (2015). Tree automata-based refinement with application to Horn clause verification. In D. D'Souza, A. Lal, & K. G. Larsen (Eds.), Verification, Model Checking, and Abstract Interpretation (Vol. 8931, pp. 209-226). Springer. Lecture Notes in Computer Science, No. 8931 https://doi.org/10.1007/978-3-662-46081-8_12
Kafle, Bishoksan ; Gallagher, John Patrick. / Tree automata-based refinement with application to Horn clause verification. Verification, Model Checking, and Abstract Interpretation. editor / Deepak D'Souza ; Akash Lal ; Kim Guldstrand Larsen. Vol. 8931 Springer, 2015. pp. 209-226 (Lecture Notes in Computer Science; No. 8931).
@inproceedings{b83018ab2555491ba02b6f502bc92e30,
title = "Tree automata-based refinement with application to Horn clause verification",
abstract = "In this paper we apply tree-automata techniques to refinement of abstract interpretation in Horn clause verification. We go beyond previous work on refining trace abstractions; firstly we handle tree automata rather than string automata and thereby can capture traces in any Horn clause derivations rather than just transition systems; secondly, we show how algorithms manipulating tree automata interact with abstract interpretations, establishing progress in refinement and generating refined clauses that eliminate causes of imprecision. We show how to derive a refined set of Horn clauses in which given infeasible traces have been eliminated, using a recent optimised algorithm for tree automata determinisation. We also show how we can introduce disjunctive abstractions selectively by splitting states in the tree automaton. The approach is independent of the abstract domain and constraint theory underlying the Horn clauses. Experiments using linear constraint problems and the abstract domain of convex polyhedra show that the refinement technique is practical and that iteration of abstract interpretation with tree automata-based refinement solves many challenging Horn clause verification problems. We compare the results with other state of the art Horn clause verification tools.",
keywords = "finite tree automata, Abstract Interpretation, Horn clauses",
author = "Bishoksan Kafle and Gallagher, {John Patrick}",
note = "@inproceedings{DBLP:conf/vmcai/KafleG15, author = {Bishoksan Kafle and John P. Gallagher}, title = {Tree Automata-Based Refinement with Application to Horn Clause Verification}, booktitle = {Verification, Model Checking, and Abstract Interpretation - 16th International Conference, {VMCAI} 2015, Mumbai, India, January 12-14, 2015. Proceedings}, pages = {209--226}, year = {2015}, crossref = {DBLP:conf/vmcai/2015}, url = {http://dx.doi.org/10.1007/978-3-662-46081-8_12}, doi = {10.1007/978-3-662-46081-8_12}, timestamp = {Fri, 12 Dec 2014 12:30:11 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/KafleG15}, bibsource = {dblp computer science bibliography, http://dblp.org} } @proceedings{DBLP:conf/vmcai/2015, editor = {Deepak D'Souza and Akash Lal and Kim Guldstrand Larsen}, title = {Verification, Model Checking, and Abstract Interpretation - 16th International Conference, {VMCAI} 2015, Mumbai, India, January 12-14, 2015. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {8931}, publisher = {Springer}, year = {2014}, url = {http://dx.doi.org/10.1007/978-3-662-46081-8}, doi = {10.1007/978-3-662-46081-8}, isbn = {978-3-662-46080-1}, timestamp = {Fri, 12 Dec 2014 12:27:22 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/2015}, bibsource = {dblp computer science bibliography, http://dblp.org} }",
year = "2015",
doi = "10.1007/978-3-662-46081-8_12",
language = "English",
isbn = "978-3-662-46080-1",
volume = "8931",
pages = "209--226",
editor = "Deepak D'Souza and Akash Lal and Larsen, {Kim Guldstrand}",
booktitle = "Verification, Model Checking, and Abstract Interpretation",
publisher = "Springer",

}

Kafle, B & Gallagher, JP 2015, Tree automata-based refinement with application to Horn clause verification. in D D'Souza, A Lal & KG Larsen (eds), Verification, Model Checking, and Abstract Interpretation. vol. 8931, Springer, Lecture Notes in Computer Science, no. 8931, pp. 209-226, 16th International Conference on Verification, Model Checking, and Abstract Interpretation, Mumbai, India, 12/01/2015. https://doi.org/10.1007/978-3-662-46081-8_12

Tree automata-based refinement with application to Horn clause verification. / Kafle, Bishoksan; Gallagher, John Patrick.

Verification, Model Checking, and Abstract Interpretation. ed. / Deepak D'Souza; Akash Lal; Kim Guldstrand Larsen. Vol. 8931 Springer, 2015. p. 209-226.

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

TY - GEN

T1 - Tree automata-based refinement with application to Horn clause verification

AU - Kafle, Bishoksan

AU - Gallagher, John Patrick

N1 - @inproceedings{DBLP:conf/vmcai/KafleG15, author = {Bishoksan Kafle and John P. Gallagher}, title = {Tree Automata-Based Refinement with Application to Horn Clause Verification}, booktitle = {Verification, Model Checking, and Abstract Interpretation - 16th International Conference, {VMCAI} 2015, Mumbai, India, January 12-14, 2015. Proceedings}, pages = {209--226}, year = {2015}, crossref = {DBLP:conf/vmcai/2015}, url = {http://dx.doi.org/10.1007/978-3-662-46081-8_12}, doi = {10.1007/978-3-662-46081-8_12}, timestamp = {Fri, 12 Dec 2014 12:30:11 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/KafleG15}, bibsource = {dblp computer science bibliography, http://dblp.org} } @proceedings{DBLP:conf/vmcai/2015, editor = {Deepak D'Souza and Akash Lal and Kim Guldstrand Larsen}, title = {Verification, Model Checking, and Abstract Interpretation - 16th International Conference, {VMCAI} 2015, Mumbai, India, January 12-14, 2015. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {8931}, publisher = {Springer}, year = {2014}, url = {http://dx.doi.org/10.1007/978-3-662-46081-8}, doi = {10.1007/978-3-662-46081-8}, isbn = {978-3-662-46080-1}, timestamp = {Fri, 12 Dec 2014 12:27:22 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/2015}, bibsource = {dblp computer science bibliography, http://dblp.org} }

PY - 2015

Y1 - 2015

N2 - In this paper we apply tree-automata techniques to refinement of abstract interpretation in Horn clause verification. We go beyond previous work on refining trace abstractions; firstly we handle tree automata rather than string automata and thereby can capture traces in any Horn clause derivations rather than just transition systems; secondly, we show how algorithms manipulating tree automata interact with abstract interpretations, establishing progress in refinement and generating refined clauses that eliminate causes of imprecision. We show how to derive a refined set of Horn clauses in which given infeasible traces have been eliminated, using a recent optimised algorithm for tree automata determinisation. We also show how we can introduce disjunctive abstractions selectively by splitting states in the tree automaton. The approach is independent of the abstract domain and constraint theory underlying the Horn clauses. Experiments using linear constraint problems and the abstract domain of convex polyhedra show that the refinement technique is practical and that iteration of abstract interpretation with tree automata-based refinement solves many challenging Horn clause verification problems. We compare the results with other state of the art Horn clause verification tools.

AB - In this paper we apply tree-automata techniques to refinement of abstract interpretation in Horn clause verification. We go beyond previous work on refining trace abstractions; firstly we handle tree automata rather than string automata and thereby can capture traces in any Horn clause derivations rather than just transition systems; secondly, we show how algorithms manipulating tree automata interact with abstract interpretations, establishing progress in refinement and generating refined clauses that eliminate causes of imprecision. We show how to derive a refined set of Horn clauses in which given infeasible traces have been eliminated, using a recent optimised algorithm for tree automata determinisation. We also show how we can introduce disjunctive abstractions selectively by splitting states in the tree automaton. The approach is independent of the abstract domain and constraint theory underlying the Horn clauses. Experiments using linear constraint problems and the abstract domain of convex polyhedra show that the refinement technique is practical and that iteration of abstract interpretation with tree automata-based refinement solves many challenging Horn clause verification problems. We compare the results with other state of the art Horn clause verification tools.

KW - finite tree automata

KW - Abstract Interpretation

KW - Horn clauses

U2 - 10.1007/978-3-662-46081-8_12

DO - 10.1007/978-3-662-46081-8_12

M3 - Article in proceedings

SN - 978-3-662-46080-1

VL - 8931

SP - 209

EP - 226

BT - Verification, Model Checking, and Abstract Interpretation

A2 - D'Souza, Deepak

A2 - Lal, Akash

A2 - Larsen, Kim Guldstrand

PB - Springer

ER -

Kafle B, Gallagher JP. Tree automata-based refinement with application to Horn clause verification. In D'Souza D, Lal A, Larsen KG, editors, Verification, Model Checking, and Abstract Interpretation. Vol. 8931. Springer. 2015. p. 209-226. (Lecture Notes in Computer Science; No. 8931). https://doi.org/10.1007/978-3-662-46081-8_12