Analysis and Transformation Tools for Constrained Horn Clause Verification

Bishoksan Kafle, John Patrick Gallagher

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

Several techniques and tools have been developed for verification of properties expressed as Horn clauses with constraints over a background theory (CHC). Current CHC verification tools implement intricate algorithms and are often limited to certain subclasses of CHC problems. Our aim in this work is to investigate the use of a combination of off-the-shelf techniques from the literature in analysis and transformation of Constraint Logic Programs (CLPs) to solve challenging CHC verification problems. We find that many problems can be solved using a combination of tools based on well-known techniques from abstract interpretation, semantics-preserving transformations, program specialisation and query-answer transformations. This gives insights into the design of automatic, more general CHC verification tools based on a library of components.
Original languageEnglish
Article number4-5
JournalTheory and Practice of Logic Programming
Volume14
Issue number4-5
Pages (from-to)90-101
Number of pages12
ISSN1471-0684
Publication statusPublished - 21 Jul 2014
Event30th International Conference on Logic Programming - Vienna, Austria
Duration: 19 Jul 201422 Jul 2014
Conference number: 30

Conference

Conference30th International Conference on Logic Programming
Number30
CountryAustria
CityVienna
Period19/07/201422/07/2014

Keywords

  • Constraint Logic Program
  • Constrained Horn clause
  • Abstract Interpretation
  • Software Verification

Cite this

@article{9d4792f7ee5248a883e78c82609b98de,
title = "Analysis and Transformation Tools for Constrained Horn Clause Verification",
abstract = "Several techniques and tools have been developed for verification of properties expressed as Horn clauses with constraints over a background theory (CHC). Current CHC verification tools implement intricate algorithms and are often limited to certain subclasses of CHC problems. Our aim in this work is to investigate the use of a combination of off-the-shelf techniques from the literature in analysis and transformation of Constraint Logic Programs (CLPs) to solve challenging CHC verification problems. We find that many problems can be solved using a combination of tools based on well-known techniques from abstract interpretation, semantics-preserving transformations, program specialisation and query-answer transformations. This gives insights into the design of automatic, more general CHC verification tools based on a library of components.",
keywords = "Constraint Logic Program, Constrained Horn clause, Abstract Interpretation, Software Verification",
author = "Bishoksan Kafle and Gallagher, {John Patrick}",
year = "2014",
month = "7",
day = "21",
language = "English",
volume = "14",
pages = "90--101",
journal = "Theory and Practice of Logic Programming",
issn = "1471-0684",
publisher = "Cambridge University Press",
number = "4-5",

}

Analysis and Transformation Tools for Constrained Horn Clause Verification. / Kafle, Bishoksan; Gallagher, John Patrick.

In: Theory and Practice of Logic Programming, Vol. 14, No. 4-5, 4-5, 21.07.2014, p. 90-101.

Research output: Contribution to journalJournal articleResearchpeer-review

TY - JOUR

T1 - Analysis and Transformation Tools for Constrained Horn Clause Verification

AU - Kafle, Bishoksan

AU - Gallagher, John Patrick

PY - 2014/7/21

Y1 - 2014/7/21

N2 - Several techniques and tools have been developed for verification of properties expressed as Horn clauses with constraints over a background theory (CHC). Current CHC verification tools implement intricate algorithms and are often limited to certain subclasses of CHC problems. Our aim in this work is to investigate the use of a combination of off-the-shelf techniques from the literature in analysis and transformation of Constraint Logic Programs (CLPs) to solve challenging CHC verification problems. We find that many problems can be solved using a combination of tools based on well-known techniques from abstract interpretation, semantics-preserving transformations, program specialisation and query-answer transformations. This gives insights into the design of automatic, more general CHC verification tools based on a library of components.

AB - Several techniques and tools have been developed for verification of properties expressed as Horn clauses with constraints over a background theory (CHC). Current CHC verification tools implement intricate algorithms and are often limited to certain subclasses of CHC problems. Our aim in this work is to investigate the use of a combination of off-the-shelf techniques from the literature in analysis and transformation of Constraint Logic Programs (CLPs) to solve challenging CHC verification problems. We find that many problems can be solved using a combination of tools based on well-known techniques from abstract interpretation, semantics-preserving transformations, program specialisation and query-answer transformations. This gives insights into the design of automatic, more general CHC verification tools based on a library of components.

KW - Constraint Logic Program

KW - Constrained Horn clause

KW - Abstract Interpretation

KW - Software Verification

M3 - Journal article

VL - 14

SP - 90

EP - 101

JO - Theory and Practice of Logic Programming

JF - Theory and Practice of Logic Programming

SN - 1471-0684

IS - 4-5

M1 - 4-5

ER -