Symbolic verification method for definite iterations over tuples of altered data structures

In order to extend the area of application of the symbolic verification method [19, 20, 21, 22, 23], definite iterations over tuples of altered data structures are introduced and reduced to the standard definite iterations. This reduction is extended to definite iterations including the exit statement. The generalization of the symbolic verification method allows us to apply it to pointer programs. As a case of study, programs over doubly-linked lists are considered. A program that merges in-place ordered doubly-linked lists is verified by the symbolic method.