An iterative approach to precondition inference using constrained Horn clauses

Bishoksan Kafle, John Patrick Gallagher, Graeme Gange, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assertions in the program are not violated. Constrained Horn clauses (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set of unsafe initial states. The precondition then is the constraint corresponding to the complement of that set, under-approximating the set of safe initial states. This idea of complementation is not new, but previous attempts to exploit it have suffered from the loss of precision. Here we develop an iterative specialisation algorithm to give more precise, and in some cases optimal safety conditions. The algorithm combines existing transformations, namely constraint specialisation, partial evaluation and a trace elimination transformation. The last two of these transformations perform polyvariant specialisation, leading to disjunctive constraints which improve precision. The algorithm is implemented and tested on a benchmark suite of programs from the literature in precondition inference and software verification competitions.
We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assertions in the program are not violated. Constrained Horn clauses (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set of unsafe initial states. The precondition then is the constraint corresponding to the complement of that set, under-approximating the set of safe initial states. This idea of complementation is not new, but previous attempts to exploit it have suffered from the loss of precision. Here we develop an iterative specialisation algorithm to give more precise, and in some cases optimal safety conditions. The algorithm combines existing transformations, namely constraint specialisation, partial evaluation and a trace elimination transformation. The last two of these transformations perform polyvariant specialisation, leading to disjunctive constraints which improve precision. The algorithm is implemented and tested on a benchmark suite of programs from the literature in precondition inference and software verification competitions.
LanguageEnglish
JournalTheory and Practice of Logic Programming
Volume18
Issue number3-4
Pages553-570
ISSN1471-0684
DOIs
StatePublished - Jul 2018

Keywords

  • Logic programming
  • program analysis
  • program transformation
  • Program verification
  • precondition analysis

Cite this

Kafle, Bishoksan ; Gallagher, John Patrick ; Gange, Graeme ; Schachte, Peter ; Søndergaard, Harald ; Stuckey, Peter J./ An iterative approach to precondition inference using constrained Horn clauses. In: Theory and Practice of Logic Programming. 2018 ; Vol. 18, No. 3-4. pp. 553-570
@article{37dac3fdab444ddcafb315346e4cea63,
title = "An iterative approach to precondition inference using constrained Horn clauses",
abstract = "We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assertions in the program are not violated. Constrained Horn clauses (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set of unsafe initial states. The precondition then is the constraint corresponding to the complement of that set, under-approximating the set of safe initial states. This idea of complementation is not new, but previous attempts to exploit it have suffered from the loss of precision. Here we develop an iterative specialisation algorithm to give more precise, and in some cases optimal safety conditions. The algorithm combines existing transformations, namely constraint specialisation, partial evaluation and a trace elimination transformation. The last two of these transformations perform polyvariant specialisation, leading to disjunctive constraints which improve precision. The algorithm is implemented and tested on a benchmark suite of programs from the literature in precondition inference and software verification competitions.",
keywords = "Logic programming, program analysis, program transformation, Program verification, precondition analysis",
author = "Bishoksan Kafle and Gallagher, {John Patrick} and Graeme Gange and Peter Schachte and Harald S{\o}ndergaard and Stuckey, {Peter J.}",
year = "2018",
month = "7",
doi = "10.1017/S1471068418000091",
language = "English",
volume = "18",
pages = "553--570",
journal = "Theory and Practice of Logic Programming",
issn = "1471-0684",
publisher = "Cambridge University Press",
number = "3-4",

}

Kafle, B, Gallagher, JP, Gange, G, Schachte, P, Søndergaard, H & Stuckey, PJ 2018, 'An iterative approach to precondition inference using constrained Horn clauses' Theory and Practice of Logic Programming, vol. 18, no. 3-4, pp. 553-570. DOI: 10.1017/S1471068418000091

An iterative approach to precondition inference using constrained Horn clauses. / Kafle, Bishoksan; Gallagher, John Patrick; Gange, Graeme; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.

In: Theory and Practice of Logic Programming, Vol. 18, No. 3-4, 07.2018, p. 553-570.

Research output: Contribution to journalJournal articleResearchpeer-review

TY - JOUR

T1 - An iterative approach to precondition inference using constrained Horn clauses

AU - Kafle,Bishoksan

AU - Gallagher,John Patrick

AU - Gange,Graeme

AU - Schachte,Peter

AU - Søndergaard,Harald

AU - Stuckey,Peter J.

PY - 2018/7

Y1 - 2018/7

N2 - We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assertions in the program are not violated. Constrained Horn clauses (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set of unsafe initial states. The precondition then is the constraint corresponding to the complement of that set, under-approximating the set of safe initial states. This idea of complementation is not new, but previous attempts to exploit it have suffered from the loss of precision. Here we develop an iterative specialisation algorithm to give more precise, and in some cases optimal safety conditions. The algorithm combines existing transformations, namely constraint specialisation, partial evaluation and a trace elimination transformation. The last two of these transformations perform polyvariant specialisation, leading to disjunctive constraints which improve precision. The algorithm is implemented and tested on a benchmark suite of programs from the literature in precondition inference and software verification competitions.

AB - We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assertions in the program are not violated. Constrained Horn clauses (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set of unsafe initial states. The precondition then is the constraint corresponding to the complement of that set, under-approximating the set of safe initial states. This idea of complementation is not new, but previous attempts to exploit it have suffered from the loss of precision. Here we develop an iterative specialisation algorithm to give more precise, and in some cases optimal safety conditions. The algorithm combines existing transformations, namely constraint specialisation, partial evaluation and a trace elimination transformation. The last two of these transformations perform polyvariant specialisation, leading to disjunctive constraints which improve precision. The algorithm is implemented and tested on a benchmark suite of programs from the literature in precondition inference and software verification competitions.

KW - Logic programming

KW - program analysis

KW - program transformation

KW - Program verification

KW - precondition analysis

UR - https://arxiv.org/abs/1804.05989

U2 - 10.1017/S1471068418000091

DO - 10.1017/S1471068418000091

M3 - Journal article

VL - 18

SP - 553

EP - 570

JO - Theory and Practice of Logic Programming

T2 - Theory and Practice of Logic Programming

JF - Theory and Practice of Logic Programming

SN - 1471-0684

IS - 3-4

ER -

Kafle B, Gallagher JP, Gange G, Schachte P, Søndergaard H, Stuckey PJ. An iterative approach to precondition inference using constrained Horn clauses. Theory and Practice of Logic Programming. 2018 Jul;18(3-4):553-570. Available from, DOI: 10.1017/S1471068418000091