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

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

doi:10.1007/978-3-319-41528-4_14

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 proceeding › Article in proceedings › Research › peer-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 language	English
Title of host publication	Computer Aided Verification : 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I
Editors	Swarat Chaudhuri, Azadeh Farzan
Number of pages	8
Volume	Part 1
Publisher	Springer
Publication date	2016
Pages	261-268
ISBN (Print)	978-3-319-41527-7
DOIs	https://doi.org/10.1007/978-3-319-41528-4_14
Publication status	Published - 2016
Event	Computer Aided Verification: International Conference - University of Toronto in the the Bahen Centre for Information Technology , Toronto, Canada Duration: 17 Jul 2016 → 23 Jul 2016 http://i-cav.org/2016/ (Link to Conference)

Conference

Conference	Computer Aided Verification
Location	University of Toronto in the the Bahen Centre for Information Technology
Country/Territory	Canada
City	Toronto
Period	17/07/2016 → 23/07/2016
Internet address	http://i-cav.org/2016/ (Link to Conference)

Series	Lecture Notes in Computer Science
Number	9779
ISSN	0302-9743

Keywords

Automatic verification
Abstract Interpretation
Horn clauses
finite tree automata

Link to document

10.1007/978-3-319-41528-4_14

ICT-Energy
Gallagher, J. P., Rosendahl, M. & Bohr, N.
01/10/2013 → 30/09/2016
Project: Research
ENTRA: Whole-Systems Energy Transparency
Gallagher, J. P., Rosendahl, M., Rhiger, M., Strand, D. L. & Bohr, N.
01/10/2012 → 30/09/2015
Project: Research

Cite this

Kafle, B., Gallagher, J. P., & Morales, J. F. (2016). Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata. In S. Chaudhuri, & A. Farzan (Eds.), Computer Aided Verification : 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I (Vol. Part 1, pp. 261-268). Springer. Lecture Notes in Computer Science No. 9779 https://doi.org/10.1007/978-3-319-41528-4_14

Kafle, Bishoksan ; Gallagher, John Patrick ; Morales, José F. / Rahft : A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata. Computer Aided Verification : 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. editor / Swarat Chaudhuri ; Azadeh Farzan. Vol. Part 1 Springer, 2016. pp. 261-268 (Lecture Notes in Computer Science; No. 9779).

@inproceedings{5f2d0d02e70648d39e855adde4135d01,

title = "Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata",

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.",

keywords = "Automatic verification, Abstract Interpretation, Horn clauses, finite tree automata",

author = "Bishoksan Kafle and Gallagher, {John Patrick} and Morales, {Jos{\'e} F.}",

year = "2016",

doi = "10.1007/978-3-319-41528-4_14",

language = "English",

isbn = "978-3-319-41527-7",

volume = "Part 1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

number = "9779",

pages = "261--268",

editor = "Swarat Chaudhuri and Azadeh Farzan",

booktitle = "Computer Aided Verification",

note = "Computer Aided Verification : International Conference, CAV 2016 ; Conference date: 17-07-2016 Through 23-07-2016",

url = "http://i-cav.org/2016/",

}

Kafle, B, Gallagher, JP & Morales, JF 2016, Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata. in S Chaudhuri & A Farzan (eds), Computer Aided Verification : 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. vol. Part 1, Springer, Lecture Notes in Computer Science, no. 9779, pp. 261-268, Computer Aided Verification, Toronto, Canada, 17/07/2016. https://doi.org/10.1007/978-3-319-41528-4_14

Rahft : A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata. / Kafle, Bishoksan; Gallagher, John Patrick; Morales, José F.

Computer Aided Verification : 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. ed. / Swarat Chaudhuri; Azadeh Farzan. Vol. Part 1 Springer, 2016. p. 261-268 (Lecture Notes in Computer Science; No. 9779).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Rahft

T2 - Computer Aided Verification

AU - Kafle, Bishoksan

AU - Gallagher, John Patrick

AU - Morales, José F.

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

KW - Automatic verification

KW - Abstract Interpretation

KW - Horn clauses

KW - finite tree automata

U2 - 10.1007/978-3-319-41528-4_14

DO - 10.1007/978-3-319-41528-4_14

M3 - Article in proceedings

SN - 978-3-319-41527-7

VL - Part 1

T3 - Lecture Notes in Computer Science

SP - 261

EP - 268

BT - Computer Aided Verification

A2 - Chaudhuri, Swarat

A2 - Farzan, Azadeh

PB - Springer

Y2 - 17 July 2016 through 23 July 2016

ER -

Kafle B, Gallagher JP, Morales JF. Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata. In Chaudhuri S, Farzan A, editors, Computer Aided Verification : 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. Vol. Part 1. Springer. 2016. p. 261-268. (Lecture Notes in Computer Science; No. 9779). doi: 10.1007/978-3-319-41528-4_14

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

Abstract

Conference

Keywords

Link to document

Projects

ICT-Energy

ENTRA: Whole-Systems Energy Transparency

Cite this