Inria
Inria.fr
Inria Channel
Showroom des démos
Alt-Ergo, preuve automatique pour la certification de code critique
Alt-Ergo est un logiciel pour la démonstration automatique de théorèmes. Il est dédié à la preuve déductive de programmes, qui réduit la correction d'un programme par rapport à sa spécification à la validité d'une formule logique. En particulier, Alt-ergo est situé en bout de chaîne de plate-formes de preuve utilisées dans l'avionique. Selon la complexité des codes analysés, ce sont des milliers de formules qu'il faut prouver. Parce qu'il n'est pas envisageable de faire toutes ces preuves à la main, l'utilisation d'un outil comme Alt-Ergo est cruciale pour le passage à l'échelle de cette approche."
La démo en vidéo
- Equipe-projet : PROVAL
- Équipe-Projet commune avec l'université Paris-Sud 11 et le CNRS (LRI)
Mots-clés : Démonstration automatique Preuve de programme Aéronautique Défense Spatial Sécurité PROVAL
Voir aussi
Les autres démos de ce secteur :
