s'authentifier
version française rss feed

hal-00763495, version 1

Automated verification of termination certificates

Frédéric Blanqui (Auteur à contacter de préférence, http://who.rocq.inria.fr/Frederic.Blanqui/) a12, Kim Quyen Ly (, http://formes.asia/people/ly.kim.quyen/) a12

15th National Symposium of Selected ICT Problems (2012)

Résumé : In order to increase user confidence, many automated theorem provers provide certificates that can be independently verified. In this paper, we report on our progress in developing a standalone tool for checking the correctness of certificates for the termination of term rewrite systems, and formally proving its correctness in the proof assistant Coq. To this end, we use the extraction mechanism of Coq and the library on rewriting theory and termination called CoLoR.

  • Domaine : Informatique/Logique en informatique
    Informatique/Génie logiciel
    Informatique/Logiciel mathématique
  • Mots-clés : certification – termination – rewriting – Coq – formal proof – verification – proof assistant – extraction – XML Schema
 
  • hal-00763495, version 1
  • oai:hal.inria.fr:hal-00763495
  • Contributeur : 
  • Soumis le : Mardi 11 Décembre 2012, 04:39:30
  • Dernière modification le : Mardi 11 Décembre 2012, 10:24:50
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...