Abstract FR:

L'objectif de cette thèse est d'apporter de nouvelles méthodes pour vérifier des propriétés d'accessibilité de systèmes à compteurs. Nous employons le mot "méthode" pour désigner un ensemble de théorèmes fondamentaux situant les problèmes décidables et indécidables ainsi que leurs complexités, un ensemble de théorèmes d'algorithmique ainsi que des heuristiques, choisies après expérimentations, permettant d'implémenter avec efficacité les théorèmes précédents. Ces méthodes ont été implémentées dans un nouvel outil FAST.