Vérification automatique de programmes avec structures de données dynamiques a pointeurs

Though there have already been proposed multiple approaches to automatic formal
verification (or static analysis) of programs with pointers and dynamic linked
data structures, these approaches are still far from being general (i.e. covering
all the different shapes of structures that one may encounter in practice), fully
automatic, and at the same time efficient. The goal of the present project is
thus to push the current state-of-the-art in the given area as far as possible
towards obtaining techniques for automated verification of programs with dynamic
linked data structures that would meet the above described criteria. The way the
project intends to achieve the above goal is primarily based on a further
development of the abstract regular model checking (ARMC) framework proposed by
A. Boujjani, P. Habermehl, and T. Vojnar at CAV 2004.