Verification of Imperative Programs through Transformation of Constraint Logic Programs

In this paper we consider a simple imperative programming language with integer andarray variables and we use Constraint Logic Programming (CLP) [18] as a metalanguage forrepresenting imperative programs, their executions, and the properties to be verified. We useconstraints consisting of linear equalities and inequalities over integers. Note, however, thatthe method presented here is parametric with respect to the constraint domain which is used.By following an approach originally presented in [30], a given imperative programprogand itsinterpreter are first encoded as a CLP program. Then, the proofs of the properties of interestabout the programprogare sought by analyzing that derived CLP program. In order to improvethe efficiency of that analysis, it is advisable to firstcompile-awaythe CLP interpreter of thelanguage in whichprogis written. This is done by specializing the interpreter with respect tothe given programprogusing well-knownprogram specializationtechniques [21, 30].