Preuves Par R currence Avec Ensembles Couvrants Contextuels

Le processus de certification de logiciels est dans la plupart des cas une t che laborieuse et co teuse qui n cessite aussi bien des m thodes math matiques, pour exprimer sans ambigu t et de fa on structur e le comportement attendu du logiciel, que des outils automatiques pour v rifier ses propri t s. Parmi les techniques de preuve, la r currence est parfaitement adapt e pour raisonner sur des structures de donn es non-born es, comme les entiers et les listes, ou des syst mes param tr s. Cet ouvrage comprend deux parties, l'une th orique, l'autre applicative. La premi re partie d crit un principe de preuve par r currence exprim par un syst me d'inf rence abstrait
l'aide du concept d'ensembles couvrants contextuels. L'approche est suffisamment g n rale pour repr senter la plupart des syst mes d'inf rence actuels bas s sur la r currence implicite dont celui du d monstrateur de th or mes Spike. La deuxi me partie pr sente la premi re preuve formelle de l’ quivalence entre deux algorithmes g n riques de conformit du protocole de t l communications ABR. Spike a permis de v rifier de mani re compl tement automatique la majorit des 80 lemmes de cette preuve.