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 LMV


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


20/07/2016 : [LMV] Présentation du papier de Aiken & Gray, Barrier Inference, POPL 1998
Wadoud Bousdira (LMV, Université d'Orléans) Résumé
Débute à 14 h 30. Lieu : Salle SR3, bâtiment 3IA

07/03/2016 : [LMV]
Frederic Dabrowski (Univ Orléans, LIFO, LMV) Résumé
Débute à 14 h 30. Lieu : Salle SR3, bâtiment 3IA

25/01/2016 : [LMV] Rely/guarantee reasoning
Frederic Dabrowski (Univ Orléans, LIFO, LMV) Résumé
Débute à 15 h 30. Lieu : Espace communication, bâtiment 3IA

07/09/2015 : [LMV] Démonstration automatique en logique du premier ordre avec Vampire
Simon Robillard (Chalmers University of Technology) Résumé
Débute à 11 h.

20/04/2015 : [LMV] Introduction aux logiques temporelles (3/3)
Jean-Michel Couvreur (LIFO, Université d'Orléans) Résumé
Débute à 13 h 30. Lieu : Salle SR3, bâtiment 3IA

23/03/2015 : [LMV] Introduction aux logiques temporelles (2/3)
Jean-Michel Couvreur (LIFO, Université d'Orléans) Résumé
Débute à 13 h 30. Lieu : Salle SR3, bâtiment 3IA

16/03/2015 : [LMV] Introduction à Coq (4/4)
Frédéric Dabrowski (LIFO, Université d'Orléans ) Résumé
Débute à 15 h 30. Lieu : Salle SR3, bâtiment 3IA

09/03/2015 : [LMV] Introduction aux logiques temporelles (1/3)
Jean-Michel Couvreur (LIFO, Université d'Orléans) Résumé
Débute à 13 h 30. Lieu : Salle SR3, bâtiment 3IA

02/02/2015 : [LMV] Introduction à Coq (3/4)
Frédéric Loulergue (LIFO, Université d'Orléans & Inria) Résumé
Débute à 13 h 30. Lieu : Salle SR3, bâtiment 3IA

19/01/2015 : [LMV] Introduction à Coq (2/4)
Frédéric Loulergue (LIFO, Université d'Orléans) Résumé
Débute à 13 h 30.

05/01/2015 : [LMV] Introduction à Coq (1/4)
Wadoud Bousdira (LIFO, Université d'Orléans) Résumé
Débute à 15 h 30. Lieu : Salle SR3, bâtiment 3IA

Résumés des groupes de travail


[LMV] Présentation du papier de Aiken & Gray, Barrier Inference, POPL 1998 Wadoud Bousdira, LMV, Université d'Orléans
Abstract of the paper: Many parallel programs are written in SPMD style i.e. by running the same sequential program on all processes. SPMD programs include synchronization, but it is easy to write incorrect synchronization patterns. We propose a system that verifies a program's synchronization pattern. We also propose language features to make the synchronization pattern more explicit and easily checked. We have implemented a prototype of our system for Split-C and successfully verified the synchronization structure of realistic programs. DOI: http://dx.doi.org/10.1145/268946.268974


[LMV] Frederic Dabrowski, Univ Orléans, LIFO, LMV
Présentation de l'article marquant de 2016 dans le domaine de la correction de programmes.


[LMV] Rely/guarantee reasoning Frederic Dabrowski, Univ Orléans, LIFO, LMV
The Rely/Guarantee method can be seen as a compositional version of the Owicki-Gries verification method for shared memory concurrency. It was introduced by Jones in the early 80s. Jones’s insight was to describe interference between threads using binary relations. The working group is a presentation of this method.


[LMV] Démonstration automatique en logique du premier ordre avec Vampire Simon Robillard, Chalmers University of Technology
Vampire est un système destiné à établir, de manière automatique, des preuves pour des théorèmes en logique du premier ordre. Cet exposé couvrira la méthode commune à Vampire et aux autres démonstrateurs automatiques du même type : le principe de superposition, une extension de la règle de résolution avec un traitement particulier de l'égalité. Vampire comporte aussi plusieurs optimisations qui en font un des systèmes les plus performants de sa catégorie. Le système inclut par ailleurs des extensions permettant des usages autres que la démonstration de théorèmes, tels que l'interpolation ou l'analyse de programmes. Ces aspects seront aussi abordés.


[LMV] Introduction aux logiques temporelles (3/3) Jean-Michel Couvreur, LIFO, Université d'Orléans


[LMV] Introduction aux logiques temporelles (2/3) Jean-Michel Couvreur, LIFO, Université d'Orléans


[LMV] Introduction à Coq (4/4) Frédéric Dabrowski, LIFO, Université d'Orléans
Développement d'un vérificateur de code-octet (bytecode verifier) certifié en Coq.


[LMV] Introduction aux logiques temporelles (1/3) Jean-Michel Couvreur, LIFO, Université d'Orléans


[LMV] Introduction à Coq (3/4) Frédéric Loulergue, LIFO, Université d'Orléans & Inria
Suite de l'introduction à Coq : comment écrire des preuves.


[LMV] Introduction à Coq (2/4) Frédéric Loulergue, LIFO, Université d'Orléans
Programmation fonctionnelle en Coq: types de données inductifs, fonctions, fonctions inductives. Spécifications en Coq: prédicats, prédicats inductifs. Fonctions avec pré-conditions et post-conditions.


[LMV] Introduction à Coq (1/4) Wadoud Bousdira, LIFO, Université d'Orléans
Présentation générale de Coq. Introduction à la correspondance de Curry-Howard. Démonstration.