Le processus de certification de logiciels est dans la plupart des cas une tache laborieuse et couteuse qui necessite aussi bien des methodes mathematiques, pour exprimer sans ambiguite et de facon structuree le comportement attendu du logiciel, que des outils automatiques pour verifier ses proprietes. Parmi les techniques de preuve, la recurrence est parfaitement adaptee pour raisonner sur des structures de donnees non-bornees, comme les entiers et les listes, ou des systemes parametres. Cet ouvrage comprend deux parties, l'une theorique, l'autre applicative. La premiere partie decrit un principe de preuve par recurrence exprime par un systeme d'inference abstrait a l'aide du concept d'ensembles couvrants contextuels. L'approche est suffisamment generale pour representer la plupart des systemes d'inference actuels bases sur la recurrence implicite dont celui du demonstrateur de theoremes Spike. La deuxieme partie presente la premiere preuve formelle de l'equivalence entre deux algorithmes generiques de conformite du protocole de telecommunications ABR. Spike a permis de verifier de maniere completement automatique la majorite des 80 lemmes de cette preuve."