Extracting Herbrand trees from Coq

Abstract : Software certification aims at proving the correctness of programs but in many cases, the use of external libraries allows only a conditional proof: it depends on the assumption that the libraries meet their specifications. In particular, a bug in these libraries might still impact the certified program. In this case, the difficulty that arises is to isolate the defective library function and provide a counter-example. In this paper, we show that this problem can be logically formalized as the construction of a Herbrand tree for a contradictory universal theory and address it. The solution we propose is based on a proof of Herbrand's theorem in the proof assistant Coq. Classical program extraction using Krivine's classical realizability then translates this proof into a certified program that computes Herbrand trees. Using this tree and calls to the library functions, we are able to determine which function is defective and explicitly produce a counter-example to its specification.
Type de document :
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

Contributeur : Lionel Rieg <>
Soumis le : mardi 16 avril 2013 - 15:21:19
Dernière modification le : lundi 15 octobre 2018 - 14:34:01
Document(s) archivé(s) le : lundi 3 avril 2017 - 06:06:30


  • HAL Id : ensl-00814115, version 1
  • ARXIV : 1304.4557



Lionel Rieg. Extracting Herbrand trees from Coq. 2011. 〈ensl-00814115〉



Consultations de la notice


Téléchargements de fichiers