Tree automata-based refinement with application to Horn clause verification

Bishoksan Kafle, John Patrick Gallagher

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer 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.
OriginalsprogEngelsk
TitelVerification, Model Checking, and Abstract Interpretation
RedaktørerDeepak D'Souza, Akash Lal, Kim Guldstrand Larsen
Antal sider18
Vol/bind8931
ForlagSpringer
Publikationsdato2015
Sider209-226
ISBN (Trykt)978-3-662-46080-1
DOI
StatusUdgivet - 2015
Begivenhed16th International Conference on Verification, Model Checking, and Abstract Interpretation - Mumbai, Indien
Varighed: 12 jan. 201514 jan. 2015
http://research.microsoft.com/en-us/events/vmcai2015/

Konference

Konference16th International Conference on Verification, Model Checking, and Abstract Interpretation
LandIndien
ByMumbai
Periode12/01/201514/01/2015
Internetadresse
NavnLecture Notes in Computer Science
Nummer8931
ISSN0302-9743

Citer dette

Kafle, B., & Gallagher, J. P. (2015). Tree automata-based refinement with application to Horn clause verification. I D. D'Souza, A. Lal, & K. G. Larsen (red.), Verification, Model Checking, and Abstract Interpretation (Bind 8931, s. 209-226). Springer. Lecture Notes in Computer Science, Nr. 8931 https://doi.org/10.1007/978-3-662-46081-8_12