Sites Inria

English version

Equipe de recherche TOCCATA

Certified Programs, Certified Tools, Certified Floating-Point Computations

Présentation de l'équipe


Toccata est une équipe de recherche du centre INRIA
Saclay-Île-de-France, en partenariat avec le Laboratoire de Recherche
en Informatique (CNRS & Université de Paris-Sud), faisant partie de
l'Université Paris-Saclay, et localisée à Orsay, France.

L’objectif général de l’équipe est de promouvoir la spécification
formelle et la preuve assistée par ordinateur dans le développement de
logiciels qui exigent des garanties élevées de sa sécurité et de sa
conformité vis-à-vis de son comportement prévu. Nous travaillons sur
la conception de méthodes et d'outils de vérification déductive des
programmes. Une de nos compétences originales est la capacité de mener
des preuves en utilisant simultanément des prouveurs automatiques et
des assistants de preuve, en fonction de la difficulté du programme,
et plus particulièrement de la difficulté de chaque condition de
vérification. En particulier dans le cadre du logiciel Why3, nous
voulons fournir des méthodes et des outils pour la vérification
déductive de programmes qui peuvent offrir à la fois une grande
automatisation des preuves et une haute garantie de validité. Nous
développons notre propre prouveur de théorème, Alt-Ergo, qui est non
seulement utilisé dans Why3 mais aussi dans des applications externes,
ainsi que dans notre propre outil Cubicle dédié aux programmes
concurrents.

Dans les applications industrielles, les calculs numériques sont très
courants (par ex. les logiciels de contrôle dans les transports). Ils
impliquent généralement des nombres à virgule flottante. Certains des
membres de Toccata ont une expertise internationalement reconnue en
vérification déductive de programmes impliquant des calculs en virgule
flottante. Notre travail passé comprend une nouvelle approche pour
prouver les propriétés comportementales des programmes C numériques en
utilisant Frama-C/Jessie, diverses études de cas sur des applications
de cette approche, l’utilisation du solveur Gappa pour prouver des
algorithmes numériques, et une approche pour prendre en compte les
architectures et les compilateurs dans les calculs en virgule
flottante. Nous avons aussi contribué au Manuel d’arithmétique en
virgule flottante. Une étude de cas représentative est l'analyse et la
preuve de l'erreur de méthode et l'erreur d'arrondi d'un programme
d'analyse numérique résolvant l'équation de propagation d'une
onde. Notre expérience nous a conduit à la conclusion que la
vérification des programmes numériques peut bénéficier beaucoup de la
combinaison des prouveurs automatiques et des prouveurs
interactifs. La vérification des programmes numériques est un
ace de recherche principal de Toccata.

Axes de recherche


Notre programme scientifique est structuré en quatre axes :

* vérification déductive de programme ;

* démonstration automatique ;

* formalisation et certification des langages, des outils et des systèmes;

* preuve de programmes numériques.

Les détails de chaque axe sont visibles sur la page Web de notre équipe et dans nos rapports d’activité annuels.

Relations industrielles et internationales


Nos actions de transfert industriel impliquent:

* Le laboratoire commun ProofInUse avec la PME AdaCore, pour le
  développement de la boite à outils SPARK pour la vérification
  de programmes Ada critiques pour la sécurité

* La collaboration avec la société OCamlPro pour le transfert
  industriel du prouveur automatique Alt-Ergo

Mots-clés : Vérification déductive de programmes Démonstration automatique Formalisation en logique d'ordre supérieur Programmes numériques.

Suivez Inria