Conference Proceedings

RAHFT: A tool for verifying horn clauses using abstract interpretation and finite tree automata

B Kafle, JP Gallagher, JF Morales

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Springer International Publishing | Published : 2016

Abstract

© Springer International Publishing Switzerland 2016. We present Rahft (Refinement of Abstraction in Horn clauses using Finite Tree automata), an abstraction refinement tool for verifying safety properties of programs expressed as Horn clauses. The paper describes the architecture, strength and weakness, implementation and usage aspects of the tool. Rahft loosely combines three powerful techniques for program verification: (i) program specialisation, (ii) abstract interpretation, and (iii) trace abstraction refinement in a nontrivial way, with the aim of exploiting their strengths and mitigating their weaknesses through the complementary techniques. It is interfaced with an abstract domain, ..

View full abstract

Citation metrics