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.
Document type :
Reports
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00814115
Contributor : Lionel Rieg <>
Submitted on : Tuesday, April 16, 2013 - 3:21:19 PM
Last modification on : Monday, October 15, 2018 - 2:34:01 PM
Long-term archiving on : Monday, April 3, 2017 - 6:06:30 AM

Identifiers

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

Collections

Citation

Lionel Rieg. Extracting Herbrand trees from Coq. 2011. ⟨ensl-00814115⟩

Share

Metrics

Record views

283

Files downloads

181