Résumé
Nous avons dans les précédents cours et séminaires exploré la diversité des prouveurs, chacun ayant son degré d'automatisation, d'expressivité et de sûreté. Je présenterai dans cet exposé diverses approches pour combiner ces outils dans le but de bénéficier des avantages de chacun, en portant une attention particulière à deux familles de prouveurs :
- d'une part, les prouveurs SMT, très automatisés et généralistes, mais qui ont une expressivité et une sûreté plus réduite ;
- d'autre part, les assistants de preuve, des outils très expressifs et sûrs permettant la vérification de propriétés complexes, mais peu automatisés.
Je discuterai plusieurs implantations récentes de ces diverses approches, allant de l'interaction entre prouveurs SMT et Coq grâce à Ergo, SMTCoq ou encore Why3, à la tactique automatique sledgehammer d'Isabelle, en passant par l'outil de preuve de programmes semi-automatisé F*.
