Pour répondre aux besoins de notre société, de vastes réseaux de communications sont utilisés. Ils permettent de concevoir des systèmes de processus distants, où plusieurs processus sont exécutés en différents sites d'un réseau et interagissent en communiquant. Des processus peuvent être créer dynamiquement, ce qui permet de faire varier la distribution des processus au cours du temps, c'est la programmation mobile.
Il est très difficile de prouver que le comportement d'un très gros programme est conforme à une spécification donnée. C'est encore plus délicat dans le cadre de la programmation mobile. Pourtant, nous nous devons de montrer que les systèmes mobiles que nous utilisons sont sûrs. Ainsi, dans le cadre de la téléphonie mobile, une société qui utilise un réseau de processus mobiles doit être sûre que son réseau ne demandera pas d'utiliser plus de ressources qu'elle ne peut en fournir et que les contraintes de confidentialité sur les informations qui circulent sur ce réseau ne peuvent être violées.
Notre but est de développer des analyses automatiques basées sur l'Interprétation Abstraite pour répondre à ces problèmes.