On Friday 04/06/2010, at 11h, in room Byron Beige.

Speaker: Yves Bertot.

Title: Root isolation for one variable polynomials with rational coefficients.

Abstract:
Given a one variable polynomial with rational coefficients, we want to isolate its roots. In other words, we want to find a finite list of intervals such that each interval contains exactly one root of the polynomial and each root is in one of the intervals.

The approach we study is based on Bernstein coefficients. These coefficients give a discrete approximation of the behavior of a polynomial in a given closed interval. We rely on a sufficient condition concerning these coefficients (let’s call this condition C1): if the Bernstein coefficients, taken in order, have only one alternation, then the polynomial is guaranteed to have exactly one root in the corresponding interval.

The bulk of our work is to prove condition C1.

We study the relations between the coefficients and roots of a given polynomial on a given bounded interval and the coefficients and roots of the image of this polynomial after some transformations. These transformations relate the coefficients of a polynomial in the standard monomial basis to the coefficients of another polynomial in Bernstein bases. They also relate the positive roots of a polynomial to roots of the other polynomial in some bounded interval. In fact, this establishes a relation between condition C1 and Descartes’ law of sign.

On Friday 28/05/2010, at 11h, in room Byron Beige.

Speaker: Ioana Pasca.

Title: Interval Analysis in Coq.

Abstract:
We propose a formal study of interval analysis that concentrates on theoretical aspects rather than on computational ones. In particular we are interested in conditions for regularity of interval matrices. An interval matrix is called regular if all scalar matrices included in the interval matrix have non-null determinant and it is called singular otherwise. Regularity plays a central role in solving systems of linear interval equations. Several tests for regularity are available and widely used, but sometimes rely on rather involved results, hence the interest in formally verifying such conditions of regularity. In this talk we show how we define intervals, interval matrices and operations on them in the proof assistant Coq, and verify criteria for regularity and singularity of interval matrices.

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

On Tuesday 25/05/2010, at 11h, in room Byron Blanc.

Speaker: Thomas Hutchinson.

Title: Lesser-known OCaml Features.

Abstract:
In recent years the OCaml type system has been gaining new features. However, many of these additions have not been well advertised or documented. I will discuss the use of phantom types, polymorphic variants and private types. The upcoming 3.12 release of OCaml contains many new features as well. These include polymorphic recursion, first-class modules and named type parameters. I will discuss some of these forthcoming additions.

On Tuesday 08/12/2009, at 15h30, in room Byron Blanc.

Speaker: Evgeny Makarov.

Abstract:
We propose a monadic higher-order language with recursion and mutable references where types can be annotated with pre- and postconditions in a manner similar to Hoare logic. Specifications in Hoare triples are written using separation logic, which allows expressing behavior of programs working with data structures stored in the heap, such as linked lists and trees, in a succinct local manner. Effect-free program terms may be freely used specifications, resulting in dependent types. We also describe an embedding in Coq and construction of a formalized proof of type safety.

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/