Projects per year
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.
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/Territory | 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
Projects
- 2 Finished
-
-
NUSA: Numeric and Symbolic Abstractions for Software Model Checking
Gallagher, J. P., Rosendahl, M. & Rhiger, M.
01/01/2011 → 31/12/2013
Project: Research