L’étude des langages réguliers et leur correspondance avec les automates et différents formalismes logiques ont été appliquées avec succès à la vérification de programmes. On peut citer par exemple les Logiques Temporelles, implémentées dans des outils tels que UPPAAL ou SPOT. Le fil directeur du thème Méthodes formelles pour la transduction est l’extension de ces réussites vers le formalisme des transductions, i.e. des transformations de langages formels modélisés par des automates à sortie appelés transducteurs.