Seminar details

Abstract: Dear all,
It is a great pleasure to invite you to the defense of my PhD thesis entitled
« Automated verification of termination certificates »
You are all cordially invited to the pot de thèse that will happen after in the same place.
Jury :
Mr Frédéric Blanqui, Chargé de recherche à l’INRIA, Paris, Co-Directeur de thèse
Mr David Delahaye, Maître de conférence au CNAM, Paris, Examinateur
Mme Catherine Dubois, Professeure à l’ENSIIE, Évry, Rapporteur
Mme Dominique Duval, Professeure à l’Université Joseph Fourier, Grenoble, Examinatrice
Mr Jean-François Monin, Professeur à l’Université Joseph Fourier, Grenoble, Directeur de thèse
Mr René Thiemann, Priv.-Doz. Dr. University of Innsbruck, Austria, Rapporteur
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? To express with exactness what is the expected behavior of a program, one first needs to use some formal logical language. However, as shown by Gödel, in any formal system rich enough for doing arithmetics, there are valid formulas that cannot be proved. Therefore, there is no program that can decide whether any property is true or not. However, we can have a program that decides whether any proof is correct or not, and the present work will use in an essential way such a program, namely Coq, to formally prove the correctness of some particular program.
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 termination certificate 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. 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 defined 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 and the Haskell language.