Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata

Bishoksan Kafle, John Patrick Gallagher, José F. Morales

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

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, a tool for manipulating finite tree automata and various solvers for reasoning about constraints. Its modular design and customizable components allows for experimenting with new verification techniques and tools developed for Horn clauses.
Original languageEnglish
Title of host publicationComputer Aided Verification : 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I
EditorsSwarat Chaudhuri, Azadeh Farzan
Number of pages8
VolumePart 1
PublisherSpringer
Publication date2016
Pages261-268
ISBN (Print)978-3-319-41527-7
DOIs
Publication statusPublished - 2016
EventComputer Aided Verification: International Conference - University of Toronto in the the Bahen Centre for Information Technology , Toronto, Canada
Duration: 17 Jul 201623 Jul 2016
http://i-cav.org/2016/ (Link to Conference)

Conference

ConferenceComputer Aided Verification
LocationUniversity of Toronto in the the Bahen Centre for Information Technology
CountryCanada
CityToronto
Period17/07/201623/07/2016
Internet address
SeriesLecture Notes in Computer Science
Number9779
ISSN0302-9743

Keywords

  • Automatic verification
  • Abstract Interpretation
  • Horn clauses
  • finite tree automata

Cite this