Interpolant Tree Automata and their Application in Horn Clause Verification

This paper investigates the combination of abstract interpretation over the domain of convex polyhedra with interpolant tree automata, in an abstraction-refinement scheme for Horn clause verification. These techniques have been previously applied separately, but are combined in a new way in this pap...

Full description

Bibliographic Details
Main Authors: Bishoksan Kafle, John P. Gallagher
Format: Article
Language:English
Published: Open Publishing Association 2016-07-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1601.06521v2