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.

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…

Points forts du logiciel Nubo :

  • 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.

 

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

Fiche technique

  • Equipe-Projet : Deducteam
  • Langage : Ocaml, Makefile
Domaines d'applications :

Devenez partenaire du centre Inria de Saclay

Contactez-nous pour échanger sur votre besoin

L'équipe Deducteam

Pour aller plus loin

Articles scientifiques :