查看文章

Les preuves par récurrence sont parfaitement adaptées au raisonnement sur des structures de données non-bornées, comme par exemple les entiers et les listes, ou, de manière plus générale, sur des ensembles d’éléments non-vides munis d’ordres noethériens. Leur domaine d’application est très vaste, une utilité particulière portant sur la validation des propriétés d’applications industrielles dans des domaines critiques tels que les télécommunications et les cartes à puces. Le principe de récurrence noethérienne est à la base d’un ensemble de techniques de preuve par récurrence modernes, dont celles basées sur la récurrence implicite.

Dans cette thèse, nous nous intéresserons à l’intégration du raisonnement par récurrence implicite tel qu’il est implémenté dans le démonstrateur Spike en utilisant l’environnement de preuve certifié Coq. Basé sur la récurrence implicite, Spike est capable de raisonner automatiquement sur des théories conditionnelles de premier ordre. L’implémentation de Spike n’est pas encore certifiée, même si les fondements théoriques sous-jacents ont été approuvés à plusieurs reprises par la communauté scientifique. Une alternative convenable serait de certifier seulement les preuves générées par Spike. Dans ce cas, le processus de certification doit être automatique car les scripts de preuves de Spike sont souvent longs. Des travaux précédents ont montré la possibilité de certifier automatiquement des preuves par récurrence implicite générées par Spike à l’aide de l’environnement certifié de l’assistant de preuve Coq. Nous proposerons des nouvelles tactiques Coq qui seront capables de prouver …