Journal article

An iterative approach to precondition inference using constrained Horn clauses

Bishoksan Kafle, John P Gallagher, Graeme Gange, Peter Schachte, Harald Sondergaard, Peter J Stuckey

THEORY AND PRACTICE OF LOGIC PROGRAMMING | CAMBRIDGE UNIV PRESS | Published : 2018

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

View full abstract

Grants

Awarded by Discovery Project


Awarded by Discovery Early Career Researcher Award


Funding Acknowledgements

We are grateful for support from the Australian Research Council. The work was supported by Discovery Project grant DP140102194, and Graeme Gange is supported through Discovery Early Career Researcher Award DE160100568. We wish to thank Jorge Navas, for useful discussions based on an early draft of the manuscript, Emanuele De Angelis, for making benchmarks available to us, and the three anonymous reviewers, for suggestions which led to clear improvements of the paper.