La vérification formelle de programmes informatiques ou de systèmes dits
critiques tels que dans le transport, l’énergie, etc, est essentielle pour
garantir le bon fonctionnement de ces systèmes. Les méthodes de vérification
employées s’appuient très fortement sur des procédés mathématiques et logiques
permettant de raisonner de manière formelle sur le comportement de ces systèmes.
Ces procédés définissent généralement les comportements sous forme de grands
ensembles de contraintes logiques. L’approche par satisfaisabilité est une
méthode largement utilisée pour vérifier ces contraintes et est un exemple de
cas, où les solveurs SMT (satisfaisabilité modulo théories) sont
fortement sollicités

Généralement, les solveurs SMT ne gèrent que la logique de premier ordre et ils

ne peuvent généralement pas effectuer de preuves par induction. C’est regrettable, car la
plupart des outils de vérification interactifs, qui utilisent les solveurs SMT,
utilisent des langages d’ordre supérieur.

L’objectif de cette thèse dans sa globalité est d’offrir des solutions pour
améliorer les interactions entre solveur automatique et assistant de preuves. En
particulier nous répondons à deux problématiques importantes permettant
d’améliorer les usages de solveurs SMT au sein des assistants de preuves. Notre
première contribution permet de réduire l’écart entre solveur et assistant de
preuve en proposant une architecture adaptée pour la logique d’ordre supérieur.
La seconde contribution permet d’améliorer les capacités de raisonnement des
solveurs SMT pour les quantificateurs. Pour les deux approches développées nous
apportons un ensemble d’évaluation sur des problèmes extraits pour la grande
majorité de problèmes de formalisation. Les résultats obtenus lors de ces
évaluations sont encourageants et montrent que les techniques développées dans
cette thèse peuvent apporter de bonnes améliorations pour les solveurs SMT.

Ce doctorat s’est effectué dans le cadre du projet ERC porté par Jasmin Blanchette
(Matryoshka), un projet qui vise à concevoir des
prouveurs automatiques utiles pour la vérification interactive, et réduire
l’écart entre les prouveurs interactifs et solveurs automatiques. L’un des
objectifs concrets du projet est d’étendre les capacités de raisonnement des
solveurs SMT vers l’ordre supérieur.

Mme Catherine DUBOIS, Professeur, Ecole Nationale Supérieure d’Informatique pour l’Industrie et l’Entreprise – FRANCE

Mme Chantal KELLER, Maître de conférences, LRI, Université Paris-Saclay – FRANCE