Dynamic Synthesis of Program Invariants using Genetic Programming

Symbolic program manipulation plays a key role in program comprehension and verification. Logic formulae are used to represent the program's state and transformation rules describe the effect of statement executions on the program's state. A well-known problem arises in the case of loops, since the number of iterations is generally unknown. The effect of a loop is therefore abstracted into a loop invariant, whose derivation cannot in general be automated and requires human ingenuity. In this paper, we present a preliminary approach that integrates genetic programming into the synthesis of invariant formula that describes the behavior of a loop. We present a specific representation of formulae that works well with loops manipulating arrays. The technique has been validated with a set of relevant examples with increasing complexity. The preliminary results are promising and show the feasibility of our approach.