Category: Séminaires

Séminaire Marelle : Machines d’Eilenberg Effectives

Mercredi 18/11/2009, à partir de 10h30, en salle Galois Coriolis.

Orateur : Benoit Razet.

Titre : Machines d’Eilenberg Effectives.

Résumé :
La théorie des automates est apparue pour résoudre des problèmes aussi bien pratiques que théoriques, et ceci dès le début de l’informatique. Désormais, les automates font partie des notions fondamentales de l’informatique, et se retrouvent dans beaucoup de logiciels. En 1974, Samuel Eilenberg proposa un modèle de calcul qui unifie la plupart des automates (transducteurs, automates à pile et machines de Turing) et qui a une propriété de modularité intéressante au vu d’applications reposant sur différentes couches d’automates; comme cela peut être le cas en linguistique computationnelle.

Nous proposons d’étudier les techniques permettant d’avoir des machines d’Eilenberg effectives. Cette étude commence par la modélisation de relations calculables à base de flux, puis continue avec l’étude de la simulation des machines d’Eilenberg définies avec ces relations. Le simulateur est un programme fonctionnel énumérant progressivement les solutions, en explorant un espace de recherche selon différentes stratégies. En particulier, une stratégie de recherche en profondeur d’abord est parfaitement adaptée à ce que nous appelons les machines d’Eilenberg finies, et dans ce cas nous fournissons une preuve formelle de correction du programme de simulation.

Les relations sont une première composante des machines d’Eilenberg, la deuxième composante étant son contrôle, qui est défini par un automate fini. Dans ce contexte, on peut utiliser une expression régulière comme syntaxe pour décrire la composante de contrôle d’une machine d’Eilenberg. Récemment, un ensemble de travaux utilisant la notion de dérivées de Brzozowski, a été la source d’algorithmes efficaces de synthése d’automates non-déterministes à partir d’expressions régulières. Nous faisons l’état de l’art de ces algorithmes et nous montrons comment les implémenter de manière efficace en OCaml.

PDF : http://pauillac.inria.fr/~razet/THESE/these.pdf

Séminaire Marelle : Interfacing with Coq

Désolé, cet article est seulement disponible en Anglais Américain.

Séminaire Marelle : Towards a minimal axiom system for the real numbers in Coq

Désolé, cet article est seulement disponible en Anglais Américain.

Séminaire Marelle : Certifying floating-point programs

Désolé, cet article est seulement disponible en Anglais Américain.

Séminaire Marelle : Integrating SAT solvers in Coq

Désolé, cet article est seulement disponible en Anglais Américain.

Séminaire Marelle : Formal verification of exact computation using Newton’s method

Désolé, cet article est seulement disponible en Anglais Américain.

Séminaire Marelle : Formal certification of ElGamal encryption: A gentle introduction to CertiCrypt

Désolé, cet article est seulement disponible en Anglais Américain.

Séminaire Marelle : Finite Group Representation Theory with Coq

Désolé, cet article est seulement disponible en Anglais Américain.

Séminaire Marelle : Formal certification of code-based cryptographic proofs

Désolé, cet article est seulement disponible en Anglais Américain.

Séminaire Marelle : J.C. Filliatre: Queens on a Chessboard: an Exercise in Program Verification

Désolé, cet article est seulement disponible en Anglais Américain.