Analysis and Transformation Tools for Constrained Horn Clause Verification

Bishoksan Kafle, John Patrick Gallagher

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Resumé

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.
OriginalsprogEngelsk
Artikelnummer4-5
TidsskriftTheory and Practice of Logic Programming
Vol/bind14
Udgave nummer4-5
Sider (fra-til)90-101
Antal sider12
ISSN1471-0684
StatusUdgivet - 21 jul. 2014
Begivenhed30th International Conference on Logic Programming - Vienna, Østrig
Varighed: 19 jul. 201422 jul. 2014
Konferencens nummer: 30

Konference

Konference30th International Conference on Logic Programming
Nummer30
LandØstrig
ByVienna
Periode19/07/201422/07/2014

Emneord

    Citer dette

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

    I: Theory and Practice of Logic Programming, Bind 14, Nr. 4-5, 4-5, 21.07.2014, s. 90-101.

    Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer 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 -