From pointer systems to counter systems using shape analysis
LSV, ENS de Cachan, France.
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.
Joint work with Sebastien Bardin, Alain Finkel and Etienne Lozes.