Le LACL (Laboratoire d'Algorithmique, Complexité et Logique) est un laboratoire de l'Université Paris-Est Créteil (UPEC), membre du PRES Paris-Est.
Les membres du LACL sont en grande majorité enseignants-chercheurs au département informatique de l'UFR de Sciences et de technologie, à l'ESIAG, ou au département informatique de l'IUT Sénart / Fontainebleau. La plupart sont impliqués dans la 2ème année du Master Sécurité des Systèmes Informatiques (SSI) à l'UPEC.
Le LACL appartient à l'école doctorale MSTIC.
Les thèmes de recherche du laboratoire s'organisent autour la définition et l'étude d'outils pour la modélisation formelle de systèmes. Le laboratoire comporte deux équipes, Logique, calcul et programmation et Spécification et vérification de systèmes. La première gravite autour des thèmes liés à la définition et l'étude de modèles formels (calcul spatial, théories logiques, automates...). La seconde se concentre sur l'étude et le développement de techniques et de méthodologies formelles d'analyse, de conception et de vérification pour différents types de systèmes (parallèles, concurrents, distribués, probabilistes, ...)
Alexis Bes, Patrick Cegielski, Julien Cervelle, Serghei Verlan, Pierre Valarcher
Le premier but de cette thématique est d'étudier la puissance et le comportement de modèles de calculs parmi les ASM (abstrait state machine), les automates cellulaires, les systèmes de réécriture ou les systèmes à membrane.
L'une des question les plus naturelles qui se posent sont des questions de décidabilité. En effet, par essence d'un modèle de calcul, la plupart des propriétés de ses calculs ou sur ses machines sont indécidables. Il est donc naturel de rechercher qu'est-ce qui rend un modèle de calcul indécidable afin d'essayer, au travers de simplifications ou de restriction, de décrire la frontière avec le décidable. Plusieurs approches sont envisagées. L'une d'elle consiste à décrire le modèle avec une théorie logique et d'affaiblir cette dernière soit en réduisant la puissance des prédicats soit en choisissant des logiques plus faibles. Une autre consiste à limiter directement les possibilités du système en contraignant les transitions possibles.
Une autre question fondamentale est de savoir si un modèle de calcul est adapté à la modélisation de systèmes. On parle alors d'expressivité. Par exemple, si les machines de Turing sont reconnues comme étant le bon modèle pour les fonctions calculables, les ASM peuvent se révéler un meilleur modèle pour les algorithmes, c'est-à-dire là où la complexité entre en jeu. De même, la modélisation des systèmes physiques se fait essentiellement par des équations différentielles. Il est cependant intéressant d'étudier comment d'autres modélisations discrètes peuvent se révéler plus pertinentes dans les systèmes complexes ou chaotiques.
Tristan Crolard, Emmanuel Polonowski, Pierre Valarcher
Nous étudions un nouveau formalisme de preuve de programmes impératif qui s'appuie sur des techniques issues de la théorie des types. Un des objectifs majeurs consiste à définir un cadre formel pour certifier des programmes impératifs et fonctionnels d'ordre supérieur utilisant des mécanismes de contrôle de flot (comme les sauts non-locaux, les continuations délimitées et les coroutines).
Les "logiques de programmes" (program logics) pour les langages impératifs prennent généralement la forme d'une "sémantique axiomatique" dans la lignée des travaux de Floyd, Hoare et Dijkstra. En comparaison, les logiques de programmes pour les programmes fonctionnels sont plus souvent basées sur l'interprétation des programmes comme des preuves (isomorphisme de Curry-Howard) qui est le fondement de la théorie des types.
Relativement peu de ponts existent entre ces deux mondes, et il est donc difficile d'exploiter des résultats obtenus en théorie des types dans le monde des logiques de programmes. Une avancée récente remarquable en théorie des types consiste en l'interprétation de mécanismes de contrôle génériques comme contenu calculatoire de raisonnements classiques (les théories des types étant traditionnellement constructives). L'intérêt de cette interprétation est en particulier d'être compatible avec la présence de variables procédurales d'ordre supérieur, cette combinaison étant par ailleurs réfractaire à l'axiomatisation sous forme de logique de Floyd-Hoare.
Le cadre formel que nous avons développé a donc pour but d'unifier ces deux points de vue afin de faire profiter les langages impératifs de ces résultats récents de théorie des types. Il peut être vu comme une théorie des types impérative classique, qui est assez expressive pour prendre en compte des sauts non-locaux et où il est donc possible d'interpréter les programmes impératifs bien typés directement comme des preuves classiques de leur spécification.
La sémantique dénotationnelle du langage impératif est au départ définie sous forme d'une traduction compositionnelle. Cette sémantique peut ensuite être raffinée en une sémantique opérationnelle qui sera simulée par la réduction de son image fonctionnelle, ou plus finement, par une machine abstraite. Le système de type dépendants du langage impératif est lui-même suffisament riche pour autoriser le plongement d'une logique de Floyd-Hoare plus traditionnelle.
Olivier Michel, Antoine Spicher
à venir
Nathalie Caspard
En tant que relations d'ordre particulières - car définissables algébriquement - les treillis ont été considérés dès la fin du XIXè siècle par Schröder et Dedekind puis sont tombés dans l'oubli avant de reparaître dans les années 1930 grâce notamment à Birkhoff, Öre et bien d'autres mathématiciens. Ce furent longtemps les principaux ordres étudiés, en partie du fait de leurs liens avec l'algèbre universelle. Historiquement, leur étude précède celle des ordres.
Au sein de la théorie des treillis, mes recherches se sont orientées essentiellement sur les treillis finis et, plus particulièrement, sur ceux qui peuvent être construits à partir du treillis à 1 élément par une suite finie d'une opération appelée la duplication d'intervalle. Il a été montré que ces treillis sont exactement les treillis bornés définis algébriquement par McKenzie. Nous avons pu, entre autres, démontrer que certaines grandes classes connues de treillis finis sont de ce type (par exemple les treillis des permutations et même, plus généralement, les treillis associés aux groupes de Coxeter finis, certains treillis de fermetures,...). J'étudie les propriétés structurelles et algorithmiques des treillis, et tente d'établir des liens entre ces propriétés et des aspects applicatifs étudiés par d'autres collègues, que ce soit en représentation des connaissances, en bases de données, en théorie du consensus ou dans certains domaines de la physique.
Joelle Cohen, Catalin Dima, Marie Duflot, Lynda Mokdad, Nihal Pekergin, Minh-Anh Tran.
La complexité croissante des systèmes rend l'analyse, l'évaluation des performances et la garantie de bon fonctionnement de plus en plus nécessaire. De plus, la prolifération de nouvelles applications et services, de nouveaux supports de transmissions et nouveaux équipements met la qualité de service (QoS), la sécurité, la vérification de propriétés temporisées, probabilistes, et quantitatives au coeur du développement de ces systèmes. La modélisation, l'évaluation des performances et la vérification deviennent des tâches essentielles, pour lesquelles il convient de développer de nouvelles méthodes afin de les adapter aux problèmes de complexité actuelle.
Dans cette thématique, les pistes suivies au LACL sont :
Catalin Dima, Frédéric Gervais, Christophe Gnaho, Régine Laleau, Farida Semmak
Dans cette thématique, les travaux de recherche portent sur la définition et l'utilisation de techniques et de notations formelles qui permettent de couvrir toutes les phases de développement de logiciels, depuis l'analyse des besoins jusqu'à l'implémentation. Les systèmes visés sont principalement les SI, en particulier les applications BD et les services web. L'objectif principal de l'équipe est la spécification et la vérification de propriétés de sûreté et de sécurité de ces systèmes.
Plus précisément, les axes de recherche sont actuellement développés :
En résumé, cette thématique vise à rechercher des techniques qui favorisent une utilisation pragmatique des méthodes formelles dans le développement de logiciels sûrs.
Fabrice Mourlin, Elisabeth Pelz
Les membres de cette thématique ont proposé et étudié divers formalismes basés sur des algèbres de réseaux de Petri colorés (M-nets, S-nets, ABCD,...) permettant :
Un deuxième thème de recherche porte sur la conception et la réalisation de mobilité d'agents en tant que principe de base d'une architecture logicielle. Cela va de la définition d'architecture par l'emploi d'algèbres de processus à la preuve de propriétés par l'usage de logiques temporelles. Des aspects novateurs étudiés concernent l'organisation d'agents au sein d'un espace de travail et la négociation d'agents lors de la migration d'un nœud à un autre du réseau. Nous appliquons nos résultats dans le cadre du calcul numérique et l'adaptation de codes existants au réseau d'exécution.
Frédéric Gava, Gaétan Hains, Sovanna Tan
D'un point de vue général, nous étudions aussi la programmation data-parallèle du point de vue des langages, du lien sémantique-performance, de son adaptation aux nouvelles plateformes métérielles (GPU, multi-cœurs, grappes dans le Cloud etc.) et de ses applications. Nous nous intéressons principalement à 3 thématiques.
Premièrement, nous travaillons au développement d'un langage de programmation de haut-niveau orienté fonctionnelle appelé BSML qui est conçu pour un modèle de parallélisme appelé BSP qui permet notamment la prédiction des performances des algorithmes sur une architecture donnée et évite les interblocages et le non-déterminisme inhérent à la concurrence. Nous nous intéressons à sa sémantique, la vérification de ses programmes, son utilisation pour l'implantation de bibliothèques ou de squelettes algorithmiques et son adaptation aux architecture parallèles modernes et hybrides (à plusieurs niveau de parallélisme).
Deuxièmement, nous travaillons sur la vérification de programme BSP en utilisant la logique de Hoare (adaptation pour BSP de l'outils WHY) et la vérification de formules CTL* pour les protocoles de sécurité en utilisant un algorithme BSP qu'on cherche aussi à vérifier en utilisant les travaux sus-mentionnés.
Dernièrement et plus récemment, nous travaillons sur une adaptation de BSML à des architectures hiérarchisées et hétérogènes mélangeant multicoeurs, GPU et autre processeurs spécialisés.
Du côté des applications nous étudions et expérimentons depuis 2 ans sur l'optimisation et la prévision de performances pour les requêtes sur documents semi-structurés, en mode flux et depuis peu aussi en mode parallèle BSML. Enfin nous avons amorcé une étude de l'application des modèles de performance à la prévisibilité dans la supervision des centres de calcul en environnement virtualisé. Le thème des masses de données est abordé par des projets autour du traitement en flux et en parallèle des requêtes sur documents XML.
| Adresse : | Secrétariat : | Directeur : |
|
LACL, département d'informatique Faculté des Sciences et Technologie 61 avenue du Général de Gaulle 94010 Créteil Cedex |
Flore TSILA Bâtiment P2 - 2ème étage - Porte 223 Tél : 01 45 17 16 47 Fax : 01 45 17 66 01 |
Régine Laleau Bâtiment P2 - 2ème étage - Porte 243 Tél : 01 45 17 65 97 |