Wyniki wyszukiwania - BazTech

1

Program Verification using Constraint Handling Rules and Array Constraint Generalizations

De Angelis E., Fioravanti F., Pettorossi A., Proietti M.

Fundamenta Informaticae

|

2017

|

Vol. 150, nr 1

73--117

EN

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 T, and we show that prog is correct by transforming T into the empty program (and thus incorrect does not hold) through the application of semantics preserving transformation rules. We can also show that prog is incorrect by transforming T into a program with the fact incorrect (and thus incorrect does hold). Some of the transformation rules perform replacements of constraints that are based on 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 CHR constraint replacements with various generalization operators on integer constraints, such as widening and convex hull. Generalization is controlled by additional constraints that relate the variable identifiers in the imperative program prog 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.

2

A Rule-based Verification Strategy for Array Manipulating Programs

De Angelis E., Fioravanti F., Pettorossi A., Proietti M.

Fundamenta Informaticae

|

2015

|

Vol. 140, nr 3/4

329--355

EN

We present a method for verifying properties of imperative programs that manipulate integer arrays. Imperative programs and their properties are represented by using Constraint Logic Programs (CLP) over integer arrays. Our method is refutational. Given a Hoare triple {ϕ} prog {ψ} that defines a partial correctness property of an imperative program prog, we encode the negation of the property as a predicate incorrect defined by a CLP program P, and we show that the property holds by proving that incorrect is not a consequence of P. Program verification is performed by applying a sequence of semantics preserving transformation rules and deriving a new CLP program T such that incorrect is a consequence of P iff it is a consequence of T . The rules are applied according to an automatic strategy whose objective is to derive a program T that satisfies one of the following properties: either (i) T is the empty set of clauses, hence proving that incorrect does not hold and prog is correct, or (ii) T contains the fact incorrect, hence proving that prog is incorrect. Our transformation strategy makes use of an axiomatization of the theory of arrays for the manipulation of array constraints, and also applies the widening and convex hull operators for the generalization of linear integer constraints. The strategy has been implemented in the VeriMAP transformation system and it has been shown to be quite effective and efficient on a set of benchmark array programs taken from the literature.

3

Proving Theorems by Program Transformation

Fioravanti F., Pettorossi A., Proietti M., Senni V.

Fundamenta Informaticae

|

2013

|

Vol. 127, nr 1-4

115--134

EN

In this paper we present an overview of the unfold/fold proof method, a method for proving theorems about programs, based on program transformation. As a metalanguage for specifying programs and program properties we adopt constraint logic programming (CLP), and we present a set of transformation rules (including the familiar unfolding and folding rules) which preserve the semantics of CLP programs. Then, we show how program transformation strategies can be used, similarly to theorem proving tactics, for guiding the application of the transformation rules and inferring the properties to be proved. We work out three examples: (i) the proof of predicate equivalences, applied to the verification of equality between CCS processes, (ii) the proof of first order formulas via an extension of the quantifier elimination method, and (iii) the proof of temporal properties of infinite state concurrent systems, by using a transformation strategy that performs program specialization.

4

Controlling Polyvariance for Specialization-based Verification

Fioravanti F., Pettorossi A., Proietti M., Senni V.

Fundamenta Informaticae

|

2013

|

Vol. 124, nr 4

483--502

EN

Program specialization has been proposed as a means of improving constraint-based analysis of infinite state reactive systems. In particular, safety properties can be specified by constraint logic programs encoding (backward or forward) reachability algorithms. These programs are then transformed, before their use for checking safety, by specializing them with respect to the initial states (in the case of backward reachability) or with respect to the unsafe states (in the case of forward reachability). By using the specialized reachability programs, we can considerably increase the number of successful verifications. An important feature of specialization algorithms is the so called polyvariance, that is, the number of specialized variants of the same predicate that are introduced by specialization. Depending on this feature, the specialization time, the size of the specialized program, and the number of successful verifications may vary. We present a specialization framework which is more general than previous proposals and provides control on polyvariance. We demonstrate, through experiments on several infinite state reactive systems, that by a careful choice of the degree of polyvariance we can design specialization-based verification procedures that are both efficient and precise.

5

Improving Reachability Analysis of Infinite State Systems by Specialization

Fioravanti F., Pettorossi A., Proietti M., Senni V.

Fundamenta Informaticae

|

2012

|

Vol. 119, nr 3/4

281-300

EN

We consider infinite state reactive systems specified by using linear constraints over the integers, and we address the problem of verifying safety properties of these systems by applying reachability analysis techniques. We propose a method based on program specialization, which improves the effectiveness of the backward and forward reachability analyses. For backward reachability our method consists in: (i) specializing the reactive system with respect to the initial states, and then (ii) applying to the specialized system the reachability analysis that works backwards from the unsafe states. For reasons of efficiency, during specialization we make use of a relaxation from integers to reals. In particular, we test the satisfiability or entailment of constraints over the real numbers, while preserving the reachability properties of the reactive systems when constraints are interpreted over the integers. For forward reachability our method works as for backward reachability, except that the role of the initial states and the unsafe states are interchanged. We have implemented our method using the MAP transformation system and the ALV verification system. Through various experiments performed on several infinite state systems, we have shown that our specialization-based verification technique considerably increases the number of successful verifications without a significant degradation of the time performance.