Lifo - Laboratoire d'Informatique Fondamentale d'orléans INSA Centre Val de Loire Université d'Orléans Université d'Orléans

Lifo > Les groupes de travail du LIFO

English Version



Contact

LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2

Email: contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37



Le groupe de travail Coq


Les différents groupes de travail : BigData Coq GAMoC LMV OSC VLAD    *TOUS*


26/03/2015 : [Coq] VMRFA - Functional Models of Hadoop
Kiminori Matsuzaki (Kochi University of Technology, Japan) Résumé
Lieu : Espace communication, bâtiment 3IA

16/03/2015 : [Coq] VMRFA - Introduction à Scala (1/2)
Ali Ed-Dbali (LIFO, Université d'Orléans) Résumé
Débute à 13 h 30. Lieu : Salle Espace Communication, bâtiment 3IA

20/02/2015 : [Coq] Introduction à Alloy & à l'API Alloy
Guesmi & Frédéric Loulergue (LIFO, Université d'Orléans & INSA Centre Val de Loire) Résumé
Débute à 09 h. Lieu : INSA CVL, Bourges

13/10/2014 : [Coq] FraDeCoPP - Preuves de programmes avec WP dans Frama-C
Virgile Prevosto (CEA LIST) Résumé
https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:tutorial:lifo-2014 / Débute à 15 h 30.

19/09/2014 : [Coq] VMRFA - Le code de MRFA_Join en Java/Hadoop commenté
Mostafa Bamha (Univ Orléans, LIFO) Résumé
Débute à 09 h. Lieu : SR3, bâtiment 3IA

08/09/2014 : [Coq] FraDeCoPP - Le problème ANSV
Simon Robillard & Frédéric Loulergue (Univ Orléans, LIFO) Résumé
Débute à 09 h. Lieu : Espace communication, bâtiment 3IA

05/09/2014 : [Coq] VMRFA - Vers la vérification de l'algorithme MRFA
Frédéric Loulergue (LIFO, Université d'Orléans) Résumé
Débute à 14 h 30. Lieu : Espace communication, bâtiment 3IA

30/06/2014 : [Coq] Analyse d'intervalles
Simon Robillard (LIFO, Université d'Orléans) Résumé
Débute à 15 h 30.

13/05/2014 : [Coq] Towards a Parallel Implementation of Powerlist Functions
Virginia Niculescu (Babes Bolya University of Cluj Napoca) Résumé
Lieu : Salle de réunion, 2e étage, bâtiment 3IA

10/03/2014 : [Coq] Présentation d'un article de OOPSLA 2013
Allan Blanchard (CEA) Résumé
Débute à 15 h 15. Lieu : Salle SR3, bâtiment 3IA

10/02/2014 : [Coq] Retour d'expérience sur l'implantation de Coq
Pierre Letouzey (PPS, Université Denis Diderot) Résumé
Débute à 15 h 30.

20/01/2014 : [Coq] Un solveur de contraintes vérifié
Catherine Dubois (ENSIIE) Résumé
Débute à 15 h 30. Lieu : Salle SR3, bâtiment 3IA

Résumés des groupes de travail


[Coq] VMRFA - Functional Models of Hadoop Kiminori Matsuzaki, Kochi University of Technology, Japan
A venir.


[Coq] VMRFA - Introduction à Scala (1/2) Ali Ed-Dbali, LIFO, Université d'Orléans
A venir.


[Coq] Introduction à Alloy & à l'API Alloy Guesmi & Frédéric Loulergue, LIFO, Université d'Orléans & INSA Centre Val de Loire


[Coq] FraDeCoPP - Preuves de programmes avec WP dans Frama-C Virgile Prevosto, CEA LIST


[Coq] VMRFA - Le code de MRFA_Join en Java/Hadoop commenté Mostafa Bamha, Univ Orléans, LIFO


[Coq] FraDeCoPP - Le problème ANSV Simon Robillard & Frédéric Loulergue, Univ Orléans, LIFO
L'objectif de la suite de séances FraDeCoPP est d'avoir un état de l'art des méthodes et outils pour la preuve de programmes, incluant un aspect pratique: la preuve de correction d'implantations du problème All Nearest Smaller Values, en séquentiel et en parallèle. La première séance: Présentation du problème ANSV et des versions prouvées correctes en Coq: séquentielle fonctionnelle et parallèle fonctionnelle, ainsi que les versions non encore prouvées correctes: séquentielle impérative, parallèle impérative. Répartition de l’étude des divers outils entre les participants.


[Coq] VMRFA - Vers la vérification de l'algorithme MRFA Frédéric Loulergue, LIFO, Université d'Orléans
L'algorithme MapReduce Frequency Adaptative (MRFA) est un algorithme très efficace pour l'évaluation de requêtes de jointure avec le framework MapReduce. L'objectif de cette séance est de présenter l'algorithme MRFA et son implantation Hadoop et avoir un aperçu du travail à réaliser pour arriver à en obtenir une version vérifiée en Coq, à partir de laquelle une implantation en Scala utilisant Hadoop pourra être extraite.


[Coq] Analyse d'intervalles Simon Robillard, LIFO, Université d'Orléans
L'analyse d'intervalles est une méthode utilisée en mathématiques depuis plus de 50 ans. Elle trouve en informatique une utilité particulière, depuis la mesure d'erreur jusqu'au développement de méthodes numériques dédiées. La représentation des réels par des intervalles permet de compléter celle par nombres à virgule flottante. Cette présentation introduira les intervalles, définira les opérations associées et présentera leurs propriétés. Différentes notions d'extension d'une fonction réelle aux intervalles seront explorées, ainsi que différentes utilisations des intervalles en informatique.


[Coq] Towards a Parallel Implementation of Powerlist Functions Virginia Niculescu, Babes Bolya University of Cluj Napoca
Current state of PL formalisation in Coq by Simon Robillard. A parallel implementation of Powerlists by Virginia Niculescu. Programming with BSML by Julien Tesson. Discussion of a parallel implementation of powerlists with BSML.


[Coq] Présentation d'un article de OOPSLA 2013 Allan Blanchard, CEA
Présentation de l'article Viktor Vafeiadis, Chinmay Narayan: Relaxed separation logic: a program logic for C11 concurrency. OOPSLA, ACM Press, 2013. http://dx.doi.org/10.1145/2509136.2509532 et discussion de l'applicabilité de cette logique pour la preuve de programmes parallèles de bas niveau, en particulier dans les systèmes d'exploitation. Mots-clés: concurrence, modèles mémoires faibles, preuve de programmes, logique de séparation Résumé de l'article: We introduce relaxed separation logic (RSL), the first program logic for reasoning about concurrent programs running under the C11 relaxed memory model. From a user's perspective, RSL is an extension of concurrent separation logic (CSL) with proof rules for the various kinds of C11 atomic accesses. As in CSL, individual threads are allowed to access non-atomically only the memory that they own, thus preventing data races. Ownership can, however, be transferred via certain atomic accesses. For SC-atomic accesses, we permit arbitrary ownership transfer; for acquire/release atomic accesses, we allow ownership transfer only in one direction; whereas for relaxed atomic accesses, we rule out ownership transfer completely. We illustrate RSL with a few simple examples and prove its soundness directly over the axiomatic C11 weak memory model.


[Coq] Retour d'expérience sur l'implantation de Coq Pierre Letouzey, PPS, Université Denis Diderot


[Coq] Un solveur de contraintes vérifié Catherine Dubois, ENSIIE