An Analysis of Permutations in Arrays

This paper is concerned with the synthesis of invariants in programs with arrays. More specifically, we consider properties concerning array contents up to a permutation. For instance, to prove a sorting procedure, one has to show that the result is sorted, but also that it is a permutation of the initial array. In order to analyze this kind of properdefine an abstract interpretation working on multisets of values, and able to discover invariant equations about such multisets.

• Type: Conference
• Year: 2010
• Where: VMCAI
• Authors: Valentin Perrelle, Nicolas Halbwachs
• Keywords: Analyze This, Formal Methods, Initial Array, Properties Concerning Array, VMCAI 2010