| 9/8/2012 |
14:00 | Byron Blanc |
Thomas Williams |
Vérification automatique de propriétés de "differential privacy" |
abstract |
| 16/12/2011 |
14:00 | Euler Violet |
Pierre-Yves Strub |
An Introduction to F*, a new dependently typed language for secure
distributed programming |
abstract |
| 7/12/2010 |
10:30 | Byron Blanc |
Yves Bertot |
Induction et co-induction mêlées |
abstract |
| 30/11/2010 |
11:00 | Byron Beige |
Loïc Pottier |
L'axiome d'univalence de Voevodsky et l'extentionnalité |
link |
| 16/11/2010 |
11:00 | Euler Bleu |
Ioana Pasca |
Vérification formelle pour les méthodes numériques |
abstract |
| 11/10/2010 |
11:00 | Euler Bleu |
Guillaume Cano |
La vérification formelle du théorème de Perron Frobenius |
abstract |
| 09/09/2010 |
16:00 | Galois Coriolis |
Sylvain Heraud |
Formaliser des fonctions polynomiales en Coq |
abstract |
| 08/07/2010 |
11:00 | Byron Blanc |
Tuan-Minh Pham |
A combination of a dynamic geometry software with a proof assistant for interactive formal proofs |
abstract
|
| 30/06/2010 |
11:00 | Byron Blanc |
Michael Armand |
De SAT a SMT |
abstract
|
| 25/06/2010 |
11:00 | Byron Blanc |
Erik Martin-Dorel |
Formalisation du lemme de Hensel en Coq |
abstract
|
| 17/06/2010 |
14:00 | Byron Blanc |
Benjamin Gregoire |
|
|
| 09/06/2010 |
11:00 | Galois Coriolis |
Nicolas Julien |
Effective and sequential definition by cases on
the reals via infinite signed-digit numerals |
abstract , pdf
|
| 04/06/2010 |
11:00 | Byron Beige |
Yves Bertot |
Root isolation for one variable polynomials with rational coefficients |
abstract
|
| 28/05/2010 |
11:00 | Byron Beige |
Ioana Pasca |
Interval Analysis in Coq |
abstract ,
pdf |
| 25/05/2010 |
11:00 | Byron Blanc |
Thomas Hutchinson |
Lesser-known OCaml Features |
abstract
|
| 8/12/2009 |
15:30 | Byron Blanc |
Evgeny Makarov |
|
abstract
|
| 18/11/2009 |
10:30 | Galois Coriolis |
Benoit Razet |
Machines d'Eilenberg Effectives |
abstract , pdf
|
| 28/09/2009 |
14:00 | Byron Blanc |
Thomas Hutchinson |
Encoding Coq's tactic language in XML |
abstract
|
| 09/07/2009 |
11:00 | Fermat Jaune |
Guillaume Allais |
Towards a minimal axiom system for the reals numbers in Coq |
abstract
|
| 12/06/2009 |
11:00 | Fermat Jaune |
Ioana Pasca |
Certifying floating-point programs |
abstract ,
pdf1,
pdf2
|
| 28/05/2009 |
10:00 | Euler Bleu |
Michael Armand |
Integrating SAT solvers in Coq |
abstract |
| 06/05/2009 |
11:00 | Fermat Jaune |
Ioana Pasca |
Formal verification of exact computation using Newton's method |
abstract ,
pdf |
| 24/04/2009 |
11:00 | Fermat Jaune |
Sylvain Heraud |
Formal certification of ElGamal encryption: A gentle introduction to CertiCrypt |
abstract ,
pdf |
| 15/04/2009 |
11:00 | Galois Coriolis |
Sidi Ould Biha |
Finite Group Representation Theory with Coq |
abstract ,
pdf |
| 30/01/2009 |
10:30 | Fermat Jaune |
Santiago Zanella |
Formal certification of code-based cryptographic proofs |
pdf |
| 9/01/2009 |
10:30 | Fermat Jaune |
Laurent Thery |
J.C. Filliatre: Queens on a Chessboard: an Exercise in Program Verification |
pdf |
| 19/12/2008 |
10:30 | Galois Coriolis |
Loic Pottier |
Connecting Grobner bases programs with Coq to do proofs in
algebra, geometry and arithmetics |
pdf |
| 12/12/2008 |
10:30 | Galois Coriolis |
Yves Bertot |
Validation of Security Mechanisms for Embedded Systems |
abstract |
