La place des logiciels ne cesse de croître dans les systèmes critiques (transports, médecine, énergie…). Les failles logicielles peuvent avoir de graves conséquences, humaines ou financières. Pour asseoir la robustesse de ces applications, les méthodes formelles, telle que l’utilisation de la preuve, simplifient le processus de vérification et en minorent le coût.

Ces méthodes sont donc indispensables dans le cadre du développement de logiciels requérant un haut niveau de confiance dans leur sûreté de fonctionnement et le respect de comportements attendus.

Plusieurs équipes du centre de recherche Inria de Saclay s’impliquent dans ce large champ de recherche.

• D’une part, pour s’assurer que le programme fait ce que le programmeur lui a dit de faire et respecte rigoureusement les spécifications d’un cahier des charges.
• D’autre part, une nouvelle problématique apparaît : les industriels ont besoin de qualifier leurs outils, c’est à dire pouvoir convaincre les organismes de certification, par exemple de l’aviation civile, que les méthodes de développement et les outils utilisés sont fiables. C’est un processus qui implique d’écrire une documentation et des textes poussés pour convaincre que le programme donne bien les bonnes réponses