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, telles que l’utilisation de la preuve, simplifient le processus de vérification et en minorent le coût.

Ces méthodes sont 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, pour accompagner les industriels qui ont besoin de convaincre les organismes de certification de la fiabilité de leurs méthodes de développement et de leurs outils. 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