Contrôle dynamique.

On étudiera les programmes comportant de la creation dynamique d´un nombre non borné de threads et les programmes multithread comportant des appels à des procedures récursives sans ou avec des paramétres.  
Pour valider l'intérêt de nos résultats, nous comptons appliquer les techniques à la vérification de programmes JAVA, un langage de programmation où tous les aspects difficiles de systèmes logiciels sont présents.