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

Automated verification of termination certificates

Abstract : Making sure that a computer program behaves as expected, especially in critical applications (health, transport, energy, communications, etc.), is more and more important, all the more so since computer programs become more and more ubiquitous and essential to the functioning of modern societies. But how to check that a program behaves as expected, in particular when the range of its inputs is very large or potentially infinite? In this work, we explain the development of a new, faster and formally proved version of Rainbow based on the extraction mechanism of Coq. The previous version of Rainbow verified a CPF le in two steps. First, it used a non-certified OCaml program to translate a CPF file into a Coq script, using the Coq libraries on rewriting theory and termination CoLoR and Coccinelle. Second, it called Coq to check the correctness of the script. This approach is interesting for it provides a way to reuse in Coq termination proofs generated by external tools. This is also the approach followed by CiME3. However, it suffers from a number of deficiencies. First, because in Coq functions are interpreted, computation is much slower than with programs written in a standard programming language and compiled into binary code. Second, because the translation from CPF to Coq is not certified, it may contain errors and either lead to the rejection of valid certificates, or to the acceptance of wrong certificates. To solve the latter problem, one needs to define and formally prove the correctness of a function checking whether a certificate is valid or not. To solve the former problem, one needs to compile this function to binary code. The present work shows how to solve these two problems by using the proof assistant Coq and its extraction mechanism to the programming language OCaml. Indeed, data structures and functions de fined in Coq can be translated to OCaml and then compiled to binary code by using the OCaml compiler. A similar approach was first initiated in CeTA using the Isabelle proof assistant.
Document type :
Complete list of metadata

Contributor : Abes Star :  Contact
Submitted on : Monday, July 3, 2017 - 9:25:06 AM
Last modification on : Friday, March 25, 2022 - 9:43:52 AM
Long-term archiving on: : Thursday, December 14, 2017 - 8:34:01 PM


Version validated by the jury (STAR)


  • HAL Id : tel-01097793, version 2



Kim Quyen Ly. Automated verification of termination certificates. Computation and Language [cs.CL]. Université de Grenoble, 2014. English. ⟨NNT : 2014GRENM036⟩. ⟨tel-01097793v2⟩



Record views


Files downloads