12 Janvier - 18 Janvier


Retour à la vue des calendrier
Mardi 13 Janvier
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Generalized paper-folding sequences
Description: Johan Nilsson
Mercredi 14 Janvier
Heure: 15:30 - 16:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Cost Linear Temporal Logic for Verification
Description: Maximilien Colange Qualitative formal verification aims at checking that a given formal property holds on a model, given as an automaton.
The automata-based approach expresses the property as an automaton then analyses its synchronisation with the model automaton.
This method can be extended with various automata flavors to handle quantitative properties.

We focus on an extension of Linear Temporal Logic (LTL) with counting capabilities: Cost Linear Temporal Logic (CLTL).
This logics can be translated into Büchi automata equipped with counters, so as to nicely extend the automata approach to model-checking.
We describe the new properties that this extension allows to handle, illustrated with examples.
We also explain how it is linked to existing qualitative LTL model-checking, and the new challenges it poses.
We also propose a CEGAR-like approach to answer compute the bounds of the values reached by the automata.
Vendredi 16 Janvier
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Approche philologique des langages de programmation
Description: Baptiste Mélès La théorie des langages de programmation s'appuie généralement sur des langages de programmation théoriques — lambda-calcul, machines de Turing, et leurs variantes — que l'on suppose représenter fidèlement — à compilation près ! — les propriétés des langages de programmation de la « vraie vie », si l'on entend par là ceux que les programmeurs utilisent pour écrire des programmes utiles au quotidien : C, C++, Perl, etc.

Or nous allons voir que les langages de programmation de la vraie vie possèdent bien des propriétés dont nul ne voudrait dans un langage théorique, et que la compilation écrase : des commandes inutiles, des redondances, des résidus purement historiques... Qui plus est, loin d'être un fait simplement négatif, ces propriétés constituent une bonne part de leur expressivité du point de vue du programmeur, et sont autant de points communs avec les langues naturelles. Nous verrons ainsi que des outils linguistiques et philologiques peuvent être mobilisés pour décrire une « sémantique du programmeur », qui échappe pour une bonne part aussi bien aux sémantiques courantes des langages de programmation qu'aux tentatives de description formelle de l'expressivité des langages de programmation.