La vérification formelle fournie des méthodes et outils pour s'assurer du bon fonctionnement d'un système. Cette thématique est à l'intersection de nombreux domaines, comme la modélisation de systèmes et de propriété, la logique pour exprimer la cohérence entre les systèmes et les propriétés à vérifier, ainsi que de nombreux autres outils impliquant la logique et les automates.