Yves BERTOT

Sorry, this entry is only available in French.

On Monday 28/09/2009, at 14h, in room Byron Blanc.

Speaker: Thomas Hutchinson.

Title: Interfacing with Coq – Encoding Coq’s tactic language in XML.

Abstract:
I will present my work on encoding the tactic language in XML. There will be a demonstration of Coq starting an external program which returns a piece of ltac. Implementation details will be discussed. Comments are requested for the direction of future work. This is a preparation for the demo I am to give at the Journées des ARC, ADT et AEx, 29/09/2009 – 01/10/2009, in Bordeaux.

On Thursday 09/07/2009, at 11h, in room Fermat Jaune.

Speaker: Guillaume Allais.

Title: Towards a minimal axiom system for the reals numbers in Coq.

Abstract:
Guillaume Allais will present his internship work. The goal is to remove the axiom from Coq’s Reals library stating that: sin(pi/2)=1. The work requires the manipulation of real analysis concepts, in particular trigonometric functions and their properties.

On Friday 12/06/2009, at 11h, in room Fermat Jaune.

Speaker: Ioana Pasca.

Title: Certifying floating-point programs.

• S. Boldo, J.C. Filliatre, G. Melquiond: Combining Coq and Gappa for Certifying Floating-Point Programs (PDF)
  

  Abstract:
  Formal verification of numerical programs is notoriously difficult. On the one hand, there exist automatic tools specialized in floating-point arithmetic, such as Gappa, but they target very restrictive logics. On the other hand, there are interactive theorem provers, such as Coq, that handle a general-purpose logic but that lack proof automation for floating-point properties. To alleviate these issues, we have implemented a mechanism for calling Gappa from a Coq interactive proof. This paper presents this combination and shows on several examples how this approach offers a significant speedup in the process of verifying floating-point programs.

• S. Boldo: Floats & Ropes: a case study for formal numerical program verification (PDF)
  

  Abstract:
  We present a case study of a formal verification of a numerical program that computes the discretization of a simple partial differential equation. Bounding the rounding error was tricky as the usual idea, that is to bound the absolute value of the error at each step, fails. Our idea is to find out a precise analytical expression that cancels with itself at the next step, and to formally prove the correctness of this approach.

On Thursday 28/05/2009, at 10h, in room Euler Bleu.

Speaker: Michaël Armand.

Title: Integrating SAT solvers in Coq.

Abstract:
Michael Armand will present his work with Benjamin Gregoire and Laurent Thery about integrating SAT solvers in Coq using certificates from an external SAT solver and an internal checker. The talk will explain SAT solving algorithms, certificates for SAT, and correctness proofs for the checker (in its state of the art!).

On Wednesday 06/05/2009, at 11h, in room Fermat Jaune.

Speaker: Ioana Pasca.

Title: Formal verification of exact computation using Newton’s method.

Abstract:
We are interested in the certification of Newton’s method. We use a formalization of the convergence and stability of the method done with the axiomatic real numbers of Coq’s Standard Library in order to validate the computation with Newton’s method done with a library of exact real arithmetic based on co-inductive streams. The contribution of this work is twofold. Firstly, based on Newton’s method, we design and prove correct an algorithm on streams for computing the root of a real function in a lazy manner. Secondly, we prove that rounding at each step in Newton’s method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. An algorithm including rounding turns out to be much more efficient.

URL: http://hal.inria.fr/inria-00369511/en/

On Friday 24/04/2009, at 11h, in room Fermat Jaune.

Speaker: Sylvain Heraud.

Title: Formal certification of ElGamal encryption: A gentle introduction to CertiCrypt.

Abstract:
CertiCrypt is a framework that assists the construction of machine-checked cryptographic proofs that can be automatically verified by third parties. To date, CertiCrypt has been used to prove formally the exact security of widely studied cryptographic systems, such as the OAEP padding scheme and the Full Domain Hash digital signature scheme. The purpose of this article is to provide a gentle introduction to CertiCrypt. For concreteness, we focus on a simple but illustrative example, namely the semantic security of the Hashed ElGamal encryption scheme in both, the standard and the random oracle model.

PDF: http://www-sop.inria.fr/members/Sylvain.Heraud/paper/fast08.pdf

On Wednesday 15/04/2009, at 10h30, in room Galois Coriolis.

Speaker: Sidi Ould Biha.

Title: Finite Group Representation Theory with Coq.

Abstract:
Representation theory is a branch of algebra that allows the study of groups through linear applications, i.e. matrices. Thus problems in abstract groups can be reduced to problems on matrices. Representation theory is the basis of character theory. In this paper we present a formalization of finite groups representation theory in the Coq system that includes a formalization of Maschke’s theorem on reducible finite group algebra.

Key-words: Representation theory, Maschke’s theorem, linear algebra, Coq, SSReflect.

URL: http://hal.inria.fr/inria-00377431/en/

On Friday 30/01/2009, at 10h30, in room Fermat Jaune.

Speaker: Santiago Zanella Béguelin.

Title: Formal certification of code-based cryptographic proofs.

PDF: http://www-sop.inria.fr/members/Santiago.Zanella/Zanella.2009.POPL.pdf

On Friday 09/01/2009, at 10h30, in room Fermat Jaune.

Speaker: Laurent Théry.

Title: J.C. Filliatre: Queens on a Chessboard: an Exercise in Program Verification.

URL: http://why.lri.fr/queens/