Automates et vérification

La vérification de programmes consiste à analyser les comportements possibles de programmes en vue de déterminer s’ils seront toujours conformes à ce qui est attendu. Pour ce faire, les caractéristiques souhaitées des comportements sont exprimées formellement et confrontées, par des techniques mathématiques rigoureuses, à l’ensemble des comportements du programme à analyser. Dans ce contexte, les automates jouent un triple rôle. Tout d’abord, ils sont fréquemment utilisés en tant que langage de programmation simplifié pour décrire les programmes à analyser. Ensuite, ils servent de formalisme de description de propriétés de comportements, soit directement, soit par traduction à partir d’un langage logique. Finalement, ils s’avèrent très utiles en tant que formalisme de description d’ensembles infinis de valeurs