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
ducteam explore les applications de la théorie de la démonstration à la conception de cadres logiques, à l’interopérabilité entre systèmes de preuves et à la construction de bibliothèques mathématiques universelles.