L'équipe projet VeriDis est commune au centre de recherche Inria Nancy–Grand Est, le Max-Planck Institut für Informatik, le CNRS et l'Université de Lorraine. Ses membres à Nancy et à Saarbrücken sont des experts en méthodes formelles et en vérification. Les missions du projet sont doubles: d'une part nous contribuons à des progrès en matière des techniques de vérification (fondées sur la preuve automatique et interactive mais aussi sur la vérification algorithmique) et de leur intégration. Notre domaine privilégié d'application est celui des algorithmes et systèmes parallèles et répartis. D'autre part nous travaillons sur les méthodes précises de conception intégrant les techniques formelles de vérification dans les processus de spécification, conception et validation de ces systèmes. 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.

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 SAT et SMT, preuves interactives, vérification algorithmique par model checking, plate-formes intégrées de vérification

Logiciels

• veriT SMT Solver
• Spass: An Automated Theorem Prover for First-Order Logic with Equality
• Redlog: Reduce Logic System

• Participation dans des projets nationaux : Decert, Vérification assistée par ordinateur de l'ordonnancement et d'accès à des ressources de programmes concurrents Java (Fondation EADS)
• Projet Tools and Methodologies for Formal Specifications and for Proofs aux Centre Commun MSR-INRIA
• SMT-SAVeS: projet INRIA-CNPq avec UFRN Natal (Brésil)