Horn clause verification with convex polyhedral abstraction and tree automata-based refinement

Bishoksan Kafle, John Patrick Gallagher

Research output: Contribution to journalJournal articleResearchpeer-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.
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.
LanguageEnglish
JournalComputer Languages, Systems and Structures
Volume47
Issue numberPart 1
Pages2-18
ISSN1477-8424
DOIs
StatePublished - Jan 2017

Keywords

  • static analysis
  • Program verification
  • tree automata

Cite this

@article{7e9efb5ce9f3412694d25b8a14d5f12c,
title = "Horn clause verification with convex polyhedral abstraction and tree automata-based refinement",
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 = "static analysis, Program verification, tree automata",
author = "Bishoksan Kafle and Gallagher, {John Patrick}",
year = "2017",
month = "1",
doi = "10.1016/j.cl.2015.11.001",
language = "English",
volume = "47",
pages = "2--18",
journal = "Computer Languages, Systems and Structures",
issn = "1477-8424",
publisher = "Pergamon Press",
number = "Part 1",

}

Horn clause verification with convex polyhedral abstraction and tree automata-based refinement. / Kafle, Bishoksan; Gallagher, John Patrick.

In: Computer Languages, Systems and Structures, Vol. 47, No. Part 1, 01.2017, p. 2-18.

Research output: Contribution to journalJournal articleResearchpeer-review

TY - JOUR

T1 - Horn clause verification with convex polyhedral abstraction and tree automata-based refinement

AU - Kafle,Bishoksan

AU - Gallagher,John Patrick

PY - 2017/1

Y1 - 2017/1

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 - static analysis

KW - Program verification

KW - tree automata

U2 - 10.1016/j.cl.2015.11.001

DO - 10.1016/j.cl.2015.11.001

M3 - Journal article

VL - 47

SP - 2

EP - 18

JO - Computer Languages, Systems and Structures

T2 - Computer Languages, Systems and Structures

JF - Computer Languages, Systems and Structures

SN - 1477-8424

IS - Part 1

ER -