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
Reports

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 metadata

Cited literature [14 references]  Display  Hide  Download

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00814115
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

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

188

Files downloads

138