Hugo HERBELIN

Chercheur Inria Paris

  • Article de bases documentaires : H3310
    Coq, assistant de preuve

    Comment assurer qu'un logiciel peut s'exécuter sans erreur dans les conditions d'application prévues ? Seule une partie des tests peut être automatisée ; pour le reste, un assistant de preuve comme Coq permet de vérifier la complétude et la logique des preuves construites dans le logiciel.