Détail d'une fiche   Version PDF

TOCCATA (SR0646IR)

Certified Programs, Certified Tools, Certified Floating-Point Computations

TOCCATA (SR0530HR) →  TOCCATA


Statut: Décision signée

Responsable : Claude Marche

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2023" : A2.1.1. Sémantique des langages de programmation , A2.1.4. Programmation fonctionnelle , A2.1.6. Programmation concurrente , A2.1.10. Langages dédiés , A2.1.11. Langages de preuve , A2.4.2. Model-checking , A2.4.3. Preuves , A6.2.1. Analyse numérique des EDP et des EDO , A7.2. Logique , A7.2.1. Procédures de décision , A7.2.2. Déduction automatique , A7.2.3. Assistants de preuve , A7.2.4. Formalisation mécanisée des mathématiques , A8.10. Arithmétique des ordinateurs

Mots-clés de "B - Autres sciences et domaines d'application - 2023" : B5.2.2. Chemin de fer , B5.2.3. Aviation , B5.2.4. Spatial , B6.1. Industrie du logiciel , B9.5.1. Informatique , B9.5.2. Mathématiques

Domaine : Algorithmique, programmation, logiciels et architectures
Thème : Preuves et vérification

Période : 01/07/2014 -> 31/12/2024
Dates d'évaluation : 17/03/2015 , 20/03/2019 ,

Etablissement(s) de rattachement : CNRS, UNIV. PARIS-SACLAY
Laboratoire(s) partenaire(s) : LMF

CRI : Centre Inria de Saclay
Localisation : UP Saclay - Laboratoire Interdisciplinaire des Sciences du Numérique Bât. 650 Ada Lovelace
Code structure Inria : 111029-2

Numéro RNSR : 201221053L
N° de structure Inria: SR0646IR

Présentation


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.


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