Résumé : : La vérification automatique connaît aujourd'hui des dévelop- pements qui la rendent applicable pour des problèmes intéressants. L'appli- cation la plus connue est la vérification de formules temporelles dans des systèmes distribués finis, souvent connue sous le nom de "model checking". Elle est aussi applicable à certains systèmes infinis, comme les systèmes temps réel, et à des logiques plus riches, comme la logique du temps alternant, qui représente les choix et les stratégies qui s'offrent à des sociétés d'agent.