Abstract FR:

Les preuves automatiques par induction sont un moyen formel pour la validation de systèmes informatiques. Dans le cadre de l'induction par ensemble test, nous proposons deux méthodes de preuves automatiques s'appliquant à des spécifications conditionnelles : l'une opérant dans les théories associatives-commutatives (AC), l'autre dans les théories observationnelles. Dans la première méthode nous proposons un calcul des schémas d'induction, ainsi qu'un système d'inférence utilisant des techniques élaborées de réécriture modulo AC. Pour une classe de spécifications, la méthode détecte toute conjecture non valide en un temps fini. Des expérimentations intéressantes sur la correction de circuits digitaux, ont produit des preuves nécessitant moins d'interaction qu'avec d'autres prouveurs connus. Dans l'approche observationnelle, les objets d'un type de données sont considérés comme égaux s'ils ne peuvent être distingués par des expérimentations à résultats observables. Ces expérimentations sont représentées par des termes particuliers appelés contextes observables. Nous proposons une méthode de preuve automatique de propriétés observationnelles reposant sur le calcul d'un ensemble fini de contextes, appelés contextes tests, qui schématise l'ensemble de tous les contextes observables. Nous proposons également des méthodes de calcul de ces contextes tests ainsi qu'un nouveau système d'inférence. Pour une classe de spécifications, la méthode détecte toute conjecture non observationnellement valide en un temps fini.