RAHFT swMATH ID: 24485 Software Authors: Kafle, B., Gallagher, J. P., Morales, J. F. Description: RAHFT: A tool for verifying Horn clauses using abstract interpretation and finite tree automata. 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 non-trivial 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. Homepage: https://link.springer.com/chapter/10.1007/978-3-319-41528-4_14 Source Code: https://github.com/bishoksan/RAHFT Related Software: z3; Ciao; SeaHorn; CiaoPP; TreeAutomizer; HSF; TRACER; JayHorn; LOGEN; MathSAT5; SMTInterpol; VeriMAP; IncA; Flix; Infer; Datalog; Spacer; Houdini; Ivy; LiquidHaskell Cited in: 6 Publications all top 5 Cited by 22 Authors 3 Hermenegildo, Manuel V. 2 Gallagher, John P. 2 Kafle, Bishoksan 2 Klemen, Maximiliano 2 López-García, Pedro 2 Morales, Jose Francisco 1 Bodik, Rastislav 1 Bueno, Francisco 1 Darmawan, Luthfi 1 Dietsch, Daniel 1 Fedyukovich, Grigory 1 Gange, Graeme 1 García-Contreras, Isabel 1 Heizmann, Matthias 1 Hoenicke, Jochen 1 Kaufman, Samuel J. 1 Liqat, Umer 1 Nutz, Alexander 1 Podelski, Andreas 1 Schachte, Peter 1 Søndergaard, Harald 1 Stuckey, Peter James Cited in 2 Serials 3 Theory and Practice of Logic Programming 1 Formal Methods in System Design Cited in 2 Fields 6 Computer science (68-XX) 3 Mathematical logic and foundations (03-XX) Citations by Year