Initiation à la preuve de programme avec Frama-C

1. Introduction

Afin de rendre les programmes plus sûrs, une approche mathématique de la programmation fut recherchée depuis les années 50. Celles-ci nous amènent à la preuve de programme, qui se caractérise comme étant la démonstration que les spécifications formelles d'un programme sont vraies. La spécification consiste à décrire très précisément ce que fait le programme. Si le programme est conforme à ses spécifications, le programme est considéré comme sûr [7][8].

À quel point un programme prouvé mathématiquement est sûr ? Et comment être sûr du vérificateur de preuve, sed quis custodiet ipsos custodes ? La sûreté du programme dépend des spécifications formulées. En effet, plusieurs classes de spécifications doivent être décrites afin d'obtenir une grande sûreté du programme. De plus, les vérificateurs de preuves font aujourd'hui encore l'objet de recherches poussées, un domaine en pleine ébullition, et de contrôles assidus (par…