Projekter pr. år
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.
Originalsprog | Engelsk |
---|---|
Titel | Computer Aided Verification : 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I |
Redaktører | Swarat Chaudhuri, Azadeh Farzan |
Antal sider | 8 |
Vol/bind | Part 1 |
Forlag | Springer |
Publikationsdato | 2016 |
Sider | 261-268 |
ISBN (Trykt) | 978-3-319-41527-7 |
DOI | |
Status | Udgivet - 2016 |
Begivenhed | 28th International Conference on Computer Aided Verification: International Conference - University of Toronto in the the Bahen Centre for Information Technology , Toronto, Canada Varighed: 17 jul. 2016 → 23 jul. 2016 http://i-cav.org/2016/ (Link til konference) |
Konference
Konference | 28th International Conference on Computer Aided Verification |
---|---|
Lokation | University of Toronto in the the Bahen Centre for Information Technology |
Land/Område | Canada |
By | Toronto |
Periode | 17/07/2016 → 23/07/2016 |
Internetadresse |
|
Navn | Lecture Notes in Computer Science |
---|---|
Nummer | 9779 |
ISSN | 0302-9743 |
Projekter
- 2 Afsluttet
-
ICT-Energy
Gallagher, J. P. (Projektdeltager), Rosendahl, M. (Projektdeltager) & Bohr, N. (Projektdeltager)
01/10/2013 → 30/09/2016
Projekter: Projekt › Forskning
-
ENTRA: Whole-Systems Energy Transparency
Gallagher, J. P. (Projektdeltager), Rosendahl, M. (Projektdeltager), Rhiger, M. (Projektdeltager), Strand, D. L. (Projektleder) & Bohr, N. (Projektdeltager)
01/10/2012 → 30/09/2015
Projekter: Projekt › Forskning