HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 metadata

Cited literature [14 references]  Display  Hide  Download

Contributor : Lionel Rieg Connect in order to contact the contributor
Submitted on : Tuesday, April 16, 2013 - 3:21:19 PM
Last modification on : Friday, September 10, 2021 - 2:34:03 PM
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⟩



Record views


Files downloads