Abstract
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 language | English |
|---|---|
| Title of host publication | Verification, Model Checking, and Abstract Interpretation |
| Editors | Deepak D'Souza, Akash Lal, Kim Guldstrand Larsen |
| Number of pages | 18 |
| Volume | 8931 |
| Publisher | Springer |
| Publication date | 2015 |
| Pages | 209-226 |
| ISBN (Print) | 978-3-662-46080-1 |
| DOIs | |
| Publication status | Published - 2015 |
| Event | 16th International Conference on Verification, Model Checking, and Abstract Interpretation - Mumbai, India Duration: 12 Jan 2015 → 14 Jan 2015 http://research.microsoft.com/en-us/events/vmcai2015/ |
Conference
| Conference | 16th International Conference on Verification, Model Checking, and Abstract Interpretation |
|---|---|
| Country | India |
| City | Mumbai |
| Period | 12/01/2015 → 14/01/2015 |
| Internet address |
| Series | Lecture Notes in Computer Science |
|---|---|
| Number | 8931 |
| ISSN | 0302-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
}
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 proceeding › Article in proceedings › Research › peer-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 -