z-logo
open-access-imgOpen Access
Program Verification using Constraint Handling Rules and Array Constraint Generalizations
Author(s) -
Emanuele De Angelis,
Maurizio Proietti,
Alberto Pettorossi,
Maurizio Proietti
Publication year - 2018
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 2398-7340
DOI - 10.29007/dkxs
Subject(s) - constraint logic programming , constraint programming , program transformation , computer science , correctness , binary constraint , theoretical computer science , generalization , integer (computer science) , transformation (genetics) , constraint (computer aided design) , mathematical optimization , constraint satisfaction , programming language , mathematics , artificial intelligence , mathematical analysis , biochemistry , chemistry , geometry , probabilistic logic , stochastic programming , gene
The transformation of constraint logic programs (CLP programs) has been shown to be an effective methodology for verifying properties of imperative programs. By following this methodology, we encode the negation of a partial correctness property of an imperative program prog as a predicate incorrect defined by a CLP program P, and we show that prog is correct by transforming P into the empty program through the application of semantics preserving transformation rules. Some of these rules perform replacements of constraints that encode properties of the data structures manipulated by the program prog. In this paper we show that Constraint Handling Rules (CHR) are a suitable formalism for representing and applying constraint replacements during the transformation of CLP programs. In particular, we consider programs that manipulate integer arrays and we present a CHR encoding of a constraint replacement strategy based on the theory of arrays. We also propose a novel generalization strategy for constraints on integer arrays that combines the CHR constraint replacement strategy with various generalization operator for linear constraints, such as widening and convex hull. Generalization is controlled by additional constraints that relate the variable identifiers in the imperative program and the CLP representation of their values. The method presented in this paper has been implemented and we have demonstrated its effectiveness on a set of benchmark programs taken from the literature.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.
Having issues? You can contact us here