théorie des automates

En informatique théorique, l'objectif de la <dfn>théorie des automates</dfn> est de proposer des modèles de mécanismes mathématiques qui formalisent les méthodes de calcul. Cette théorie est le fondement de plusieurs branches importantes de l'informatique théorique, comme :

• La calculabilité, par le modèle des machines de Turing ;
• Les automates finis, et leurs variantes, qui sont utilisés dans l'analyse des langues naturelles, la traduction des programmes par les compilateurs, divers algorithmes de manipulation de textes comme les algorithmes de recherche de sous-chaîne, ou la vérification automatique du fonctionnement de circuits logiques. C'est la partie sur laquelle on insiste le plus dans les écoles d'ingénieurs, car elle est immédiatement exploitable avec profit ;
• La théorie de la complexité des algorithmes, visant à classifier les algorithmes en fonction des ressources temporelles et en mémoire nécessaires à leur exécution ;
• La vérification de modèle qui sert à établir la conformité de programmes à leurs spécifications. Voir par exemple Coq.