Verification of Imperative Programs by Constraint Logic Program Transformation
We present a method for verifying partial correctness properties of imperative programs that manipulate integers and arrays by using techniques based on the transformation of constraint logic programs (CLP). We use CLP as a metalanguage for representing imperative programs, their executions, and the...
Main Authors: | , , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2013-09-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1309.5139v1 |
id |
doaj-de24029bfece49d1b9f91e4e8d0dc595 |
---|---|
record_format |
Article |
spelling |
doaj-de24029bfece49d1b9f91e4e8d0dc5952020-11-25T00:51:35ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-09-01129Festschrift for Dave Schmidt18621010.4204/EPTCS.129.12Verification of Imperative Programs by Constraint Logic Program TransformationEmanuele De AngelisFabio FioravantiAlberto PettorossiMaurizio ProiettiWe present a method for verifying partial correctness properties of imperative programs that manipulate integers and arrays by using techniques based on the transformation of constraint logic programs (CLP). We use CLP as a metalanguage for representing imperative programs, their executions, and their properties. First, we encode the correctness of an imperative program, say prog, as the negation of a predicate 'incorrect' defined by a CLP program T. By construction, 'incorrect' holds in the least model of T if and only if the execution of prog from an initial configuration eventually halts in an error configuration. Then, we apply to program T a sequence of transformations that preserve its least model semantics. These transformations are based on well-known transformation rules, such as unfolding and folding, guided by suitable transformation strategies, such as specialization and generalization. The objective of the transformations is to derive a new CLP program TransfT where the predicate 'incorrect' is defined either by (i) the fact 'incorrect.' (and in this case prog is not correct), or by (ii) the empty set of clauses (and in this case prog is correct). In the case where we derive a CLP program such that neither (i) nor (ii) holds, we iterate the transformation. Since the problem is undecidable, this process may not terminate. We show through examples that our method can be applied in a rather systematic way, and is amenable to automation by transferring to the field of program verification many techniques developed in the field of program transformation.http://arxiv.org/pdf/1309.5139v1 |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Emanuele De Angelis Fabio Fioravanti Alberto Pettorossi Maurizio Proietti |
spellingShingle |
Emanuele De Angelis Fabio Fioravanti Alberto Pettorossi Maurizio Proietti Verification of Imperative Programs by Constraint Logic Program Transformation Electronic Proceedings in Theoretical Computer Science |
author_facet |
Emanuele De Angelis Fabio Fioravanti Alberto Pettorossi Maurizio Proietti |
author_sort |
Emanuele De Angelis |
title |
Verification of Imperative Programs by Constraint Logic Program Transformation |
title_short |
Verification of Imperative Programs by Constraint Logic Program Transformation |
title_full |
Verification of Imperative Programs by Constraint Logic Program Transformation |
title_fullStr |
Verification of Imperative Programs by Constraint Logic Program Transformation |
title_full_unstemmed |
Verification of Imperative Programs by Constraint Logic Program Transformation |
title_sort |
verification of imperative programs by constraint logic program transformation |
publisher |
Open Publishing Association |
series |
Electronic Proceedings in Theoretical Computer Science |
issn |
2075-2180 |
publishDate |
2013-09-01 |
description |
We present a method for verifying partial correctness properties of imperative programs that manipulate integers and arrays by using techniques based on the transformation of constraint logic programs (CLP). We use CLP as a metalanguage for representing imperative programs, their executions, and their properties. First, we encode the correctness of an imperative program, say prog, as the negation of a predicate 'incorrect' defined by a CLP program T. By construction, 'incorrect' holds in the least model of T if and only if the execution of prog from an initial configuration eventually halts in an error configuration. Then, we apply to program T a sequence of transformations that preserve its least model semantics. These transformations are based on well-known transformation rules, such as unfolding and folding, guided by suitable transformation strategies, such as specialization and generalization. The objective of the transformations is to derive a new CLP program TransfT where the predicate 'incorrect' is defined either by (i) the fact 'incorrect.' (and in this case prog is not correct), or by (ii) the empty set of clauses (and in this case prog is correct). In the case where we derive a CLP program such that neither (i) nor (ii) holds, we iterate the transformation. Since the problem is undecidable, this process may not terminate. We show through examples that our method can be applied in a rather systematic way, and is amenable to automation by transferring to the field of program verification many techniques developed in the field of program transformation. |
url |
http://arxiv.org/pdf/1309.5139v1 |
work_keys_str_mv |
AT emanueledeangelis verificationofimperativeprogramsbyconstraintlogicprogramtransformation AT fabiofioravanti verificationofimperativeprogramsbyconstraintlogicprogramtransformation AT albertopettorossi verificationofimperativeprogramsbyconstraintlogicprogramtransformation AT maurizioproietti verificationofimperativeprogramsbyconstraintlogicprogramtransformation |
_version_ |
1725245011049578496 |