AVIS 2006 Preliminary Version From pointer systems to counter systems using shape analysis

We aim at checking safety properties on systems manipulating dynamic linked lists. First we prove that every pointer system is bisimilar to an effectively constructible counter system. We then deduce a two-step analysis procedure. We first build an over-approximation of the reachability set of the pointer system. If this over-approximation is too coarse to conclude, we then extract from it a bisimilar counter system which is analyzed via efficient symbolic techniques developed for general counter systems. Key words: dynamic allocation, automatic verification, counter system, pointer system, shape analysis