Seminar details

Résumé : Cette journée est ouverte à tous ceux et celles qui souhaitent en savoir plus sur l’assistant de preuve COQ. Les exposés sont à destination d’un public novice en COQ et mettent l’accent sur les motivations pour utiliser COQ, l’approche utilisée, plus que sur les détails techniques de la conduite des preuves. (Le premier exposé de la journée commencera par une brève introduction à Coq.)
L’objectif est qu’à travers 5 retours d’expérience, le public puisse se faire une idée de ce qu’on peut faire avec COQ Comment ? À quel coût ? Et bénéficier d’une expérience qui ne s’acquiert pas en suivant un tutoriel d’introduction à COQ.
EN MÉMOIRE DE V. A. VEOVODSKY
Cette journée de séminaires est dédiée à la mémoire de V.A.Veovodsky (1966-2017), mathématicien russe qui rêve d’une pratique mathématique où les résultats seraient vérifiables par un assistant de preuve. Après sa médaille Fields en 2002, il s’est attelé à étendre la théorie des types au coeur de l’assistant de preuve COQ. Son projet “fondements univalents” est en train de créer une révolution des fondements mathématiques et des assistants de preuve.
Pour en savoir plus sur V.Veovodsky
« La bifurcation de Vladimir Voevodsky. De la théorie de l'homotopie à la théorie des types », Gaz. Math., vol. 142,‎ 2014, p. 87-94 (lire en ligne)
Pour en savoir plus sur le projet fondements univalents”
- https://www.lesechos.fr/29/02/2016/LesEchos/22139-039-ECH_revolution-mathematique.htm
DETAILED PROGRAM
- 10:30-11:15 Using Coq for the formal verification of an Instruction Set Simulator
by Jean-François MONIN, VERIMAG / UGA

We present an application performed in the framework of a Sino-French cooperation : the formal verification of an Instruction Set Simulator for the ARM processor. This simulator, called SimSoC (Simulator of Systems on Chips) was designed and very efficiently implemented in C++ by another in LIAMA. For instance, it is able to boot the linux OS. In order to secure the ISS --- one of the most sensitive parts of SimSoC, we formalized in Coq the behavior of the processor; next, we got the formal behavior of (a C version of) the ISS simulator from the operational semantics of C, formalized in Coq in the Compcert Inria project, and proved that the simulator behaved accordingly to the Coq formal model. This is joint work with Xiaomu Shi, Frederic Blanqui, Claude Helmstetter and Vania Joloboff.

- 11:30-12:15 Hash consing in Coq
by David MONNIAUX, VERIMAG / CNRS

Hash consing is a technique that keeps a single copy of any immutable data structure: no isomorphic structure can be created. It is however violently imperative, which poses challenges for formalizing it in Coq. We present several approaches to this problem.

- 14:00-14:45 PADEC: A Framework for Certified Self-Stabilization
by Pierre CORBINEAU, VERIMAG / UGA
We present the PADEC framework that builds certified proofs of self-stabilizing algorithms using the proof assistant Coq. We first define in Coq the most commonly used computational model in the self-stabilizing area. We then illustrate the use of our framework by:
* certifying a non-trivial part of an existing self-stabilizing algorithm
* certifying a commonly-used composition operation for self-stabilizing algorithms
This is a joint work with Karine Altisen and Stéphane Devismes.

- 15:00-15:30 The development of a Verified Polyhedra Library made of untrusted parts mixing Ocaml, C++, threads, ... and just a little bit of Coq for certification
by Michaël PÉRIN, VERIMAG / UGA
Next year will be the 40th anniversary of the seminal paper by Cousot & Halbwachs introducing the polyhedra abstract domain. In 2013, we started the development of yet another polyhedra library, the Verimag Verified Polyhedra Library, with two goals in mind: efficiency and certification. In this talk, I will report our experience of developing a certified tool made of untrusted code with just a Coq polish.
The VPL is the result of a joint work with S.Boulmé, A.Fouilhé, A.Maréchal, D.Monniaux, M.Périn and H.Yu

- 15:45 Break

- 16:00-16:45 “Theorems for Free” (in Coq) about ML Oracles within Polymorphic LCF Style
by Sylvain BOULMÉ, VERIMAG / Grenoble INP
How can we reduce the required effort to develop certified programs in proof assistants such as Coq ? A major trend is to introduce untrusted oracles able to justify their answers by producing a certificate, ie. a witness of their computations. A trustworthy result is then built from this certificate by a certified checker. This alleviates the burden of proof, but producing certificates is a requirement which increases complexity of oracle development.
We propose a design pattern, called Polymorphic LCF Style, that removes the need for certificates: ML oracles directly compute the certified result by invoking trusted operators and data structures extracted from Coq. A strong requirement of this pattern is that oracles must only handle the trusted data structures as polymorphic values, which forbids oracles to forge incorrect results. Hence, our design pattern delegates a part of the certification to the ML typechecker.
We illustrate Polymorphic LCF Style on two examples:
* first, a refutation prover in propositional logic.
* second, the Verimag Polyhedra Library (an abstract domain of convex polyhedra).