An analysis of permutations in arrays

Abstract:
This paper is concerned with the synthesis of invariants in programs with arrays. More specifically, we consider properties concern- ing 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 proper- ties, we define an abstract interpretation working on multisets of values, and able to discover equations about such multisets.

Reference:

@inproceedings{vpnh-vmcai10
author={V. Perrelle and N. Halbwachs},
title={An analysis of permutations in arrays},
booktitle={11th International Conference on Verification, Model-checking,
        and Abstract Intepretation, VMCAI 2010},
address={Madrid, Spain},
editor={G. Barthe and M. Hemenegildo},
month=jan,
year=2010
}