Equipe de recherche VERIDIS

Modeling and Verification of Distributed Algorithms and Systems

Présentation de l'équipe

L'équipe VeriDis a pour mission d'exploiter et faire avancer les progrès en matière des techniques de preuve automatique et interactive, et leur intégration, pour la conception de systèmes parallèles et répartis. Notre but est d'assister les concepteurs à mener des projets de développement prouvé d'algorithmes et de systèmes avec la découverte automatique de preuves de propriétés intéressantes, ainsi que d'erreurs.

Les techniques de déduction automatique et interactive ont fait des progrès spectaculaires pendant la décennie passée, et ces techniques ont déjà eu un impact considérable. Par exemple, elles ont été utilisées avec succès dans la vérification et analyse de programmes séquentiels, souvent conjointement avec des techniques d'analyse statique et de model checking. Dans un monde idéal, les systèmes et leurs propriétés sont décrits dans des langage expressifs de haut niveau, les erreurs dans les spécifications sont découvertes automatiquement et enfin, une vérification complète et automatique est également effectuée. Bien évidemment ceci n'est pas possible en général, dû à la complexité inhérente à ce problème.

Néanmoins nous avons observé des progrès importants dans des techniques de preuves automatiques et interactives, auxquelles nous avons aussi contribué. Par exemple, beaucoup de progrès a été fait concernant l'intégration de théories importantes comme l'arithmétique dans des techniques de preuve symboliques. Ces progrès suggèrent qu'un degré beaucoup plus élevé d'automatisation est possible dans la vérification de systèmes, par rapport à ce que fournissent les outils actuels.

Les démonstrateurs automatiques de théorèmes ne sont pas une panacée pour la vérification de systèmes mais leur utilisation doit être fondée sur une méthodologie saine de modélisation et de vérification de systèmes. Nous avons une expertise considérable dans le développement et dans l'application de méthodes formelles dans le domaine des algorithmes et systèmes parallèles et distribués. Le concept du raffinement est central dans notre démarche. Il est important de garantir que ces méthodes viennent en soutien effectif à la conception d'algorithmes et de systèmes répartis.

Axes de recherche

langages et formalismes pour la modélisation de systèmes répartis, techniques et outils pour la preuve automatique de théorèmes, procédures de décision et solveurs SMT, preuves interactives, vérification algorithmique par model checking, plate-formes intégrées de vérification

Logiciels

Relations industrielles et internationales

Mots-clés : Méthodes formelles Preuve de théorèmes Satisfiabilité modulo théories Vérification algorithmique Systèmes répartis

Equipes de recherche du même thème :

Siège et centres de recherche Inria

Accès direct

Social