Extracting Herbrand trees from Coq - ENS de Lyon - École normale supérieure de Lyon Accéder directement au contenu
Rapport Année : 2011

Extracting Herbrand trees from Coq

Résumé

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.
Fichier principal
Vignette du fichier
tech-report2010.pdf (424.39 Ko) Télécharger le fichier
Nijmegen2011.pdf (973.69 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Format : Autre
Loading...

Dates et versions

ensl-00814115 , version 1 (16-04-2013)

Identifiants

Citer

Lionel Rieg. Extracting Herbrand trees from Coq. 2011. ⟨ensl-00814115⟩
187 Consultations
173 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More