Centre de recherche Saclay - Île-de-France

Nubo

Nubo

La bibliothèque universelle des preuves formelles

Nubo améliore et facilite la sûreté de fonctionnement et la vérification des systèmes informatiques en répondant au problème de disparité des preuves formelles, engendré par l’absence de standard et le manque d’interopérabilité des systèmes de preuves existants.

Cette base de données de preuves, traduites dans un formalisme commun facilement vérifiable*, permet aux informaticiens et aux mathématiciens de réutiliser une théorie dans un autre système, sans redémontrer toutes les preuves.

*Cette suite logicielle nommée Dedukti est également développée par l’équipe DEDUCTEAM.

L’absence de dysfonctionnements doit être garanti dans de nombreux domaines tels que les systèmes de transport, la production d’énergie, les chaînes de production de médicaments, les systèmes financiers, la robotique chirurgicale, les applications militaires…

Fiche technique

Défense & sécurité

Points forts :

  • Nubo contient des démonstrations dans les 7 systèmes les plus utilisés dans le monde : Isabelle, Zenon, Iprover, VeriT, Focalize, Matita, Hol Light.
  • Nubo a pour vocation de devenir une bibliothèque universelle de preuve formelle, en rassemblant une large communauté de contributeurs industriels et académiques, ainsi que d’organismes certificateurs.

Pour aller plus loin :

L'équipe Deducteam