TOCCATA

Toccata est une équipe de recherche du centre INRIA Saclay-Île-de-France, en partenariat avec le Laboratoire Méthodes Formelles (Université Paris-Saclay, CNRS, ENS) 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
axe de recherche principal de Toccata.