Skip to Main content Skip to Navigation

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 :
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download
Contributor : Lionel Rieg <>
Submitted on : Tuesday, April 16, 2013 - 3:21:19 PM
Last modification on : Wednesday, November 20, 2019 - 3:01:32 AM
Long-term archiving on: : Monday, April 3, 2017 - 6:06:30 AM


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



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