Tree automata-based refinement with application to Horn clause verification

Bishoksan Kafle; John Patrick Gallagher

doi:10.1007/978-3-662-46081-8_12

Tree automata-based refinement with application to Horn clause verification

Bishoksan Kafle, John Patrick Gallagher

Programming, Logic and Intelligent Systems

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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 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	https://doi.org/10.1007/978-3-662-46081-8_12
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	http://research.microsoft.com/en-us/events/vmcai2015/

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

Link to document

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

vmcai-2015-kafle-gallagherFinal published version, 305 KB

2 Finished

ENTRA: Whole-Systems Energy Transparency
Kafle, B.
EU FP7
01/10/2012 → 30/09/2015
Project: Research
NUSA: Numeric and Symbolic Abstractions for Software Model Checking
Gallagher, J. P., Rosendahl, M. & Rhiger, M.
01/01/2011 → 31/12/2013
Project: Research

Cite this

@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} }; 16th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI15 ; Conference date: 12-01-2015 Through 14-01-2015",

year = "2015",

doi = "10.1007/978-3-662-46081-8_12",

language = "English",

isbn = "978-3-662-46080-1",

volume = "8931",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

number = "8931",

pages = "209--226",

editor = "Deepak D'Souza and Akash Lal and Larsen, {Kim Guldstrand}",

booktitle = "Verification, Model Checking, and Abstract Interpretation",

url = "http://research.microsoft.com/en-us/events/vmcai2015/",

}

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 (Lecture Notes in Computer Science; No. 8931).

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

T3 - Lecture Notes in Computer Science

SP - 209

EP - 226

BT - Verification, Model Checking, and Abstract Interpretation

A2 - D'Souza, Deepak

A2 - Lal, Akash

A2 - Larsen, Kim Guldstrand

PB - Springer

T2 - 16th International Conference on Verification, Model Checking, and Abstract Interpretation

Y2 - 12 January 2015 through 14 January 2015

ER -

Tree automata-based refinement with application to Horn clause verification

Abstract

Conference

Bibliographical note

Keywords

Link to document

Projects

ENTRA: Whole-Systems Energy Transparency

NUSA: Numeric and Symbolic Abstractions for Software Model Checking

Cite this