Réunions Lande 1999-2000
 
 

Dorénavant, salle Aurigny



 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 


Calendrier des réunions
















Septembre 99
 
 
 
 
lundi  mardi  mercredi  jeudi  vendredi  samedi  dimanche 
1  2  3  4  5 
6  7  8  9  10  11  12 
13  14  15  16  17 Peter Bertelsen  18  19 
20  21  22  23  24  25  26 
27  28  29  30 

Title: Towards partial evaluation of Java bytecode
Speaker: Peter Bertelsen, KVL, Denmark
(currently visiting IRISA/project Lande) Abstract:
The Java Virtual Machine (JVM) is an abstract machine for executing Java bytecode programs. This talk describes on-going work towards partial evaluation of Java bytecode programs.
Java bytecode is an interesting target language for compilation of a broad range of programming languages. A number of efficient JVM implementations exist, and even more efficient implementations will emerge, driven by the huge interest from software industry in fast execution of Java programs. Hence, application of various program transformation techniques, e.g. partial evaluation, to Java bytecode programs seems worthwhile.
We have designed and implemented an off-line partial evaluator for a small, fairly simple core of the Java bytecode language. In this talk, I will present the core language and describe our constraint-based binding-time analysis. Our approach will be demonstrated by an example of partial evaluation of a small core language program.
We are currently working on extending the binding-time analysis and specializer to support an enriched core language with important object-oriented features: classes, objects, fields and methods. In particular, the extended analyses should support partially static objects. Current plans and ideas for this will be outlined.

Retour en haut de la page
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Octobre 99
 
 
lundi  mardi  mercredi  jeudi  vendredi  samedi  dimanche 
1  2  3 
4 Harald Sondergaard  5  6  7  8  9  10 
11  12  13  14  15 Séminaire Irisa: Daniel Pilaud  16  17 
18  19  20  21  22 Tour de Table 23  24 
25  26  27  28  29 Gaëlle Segouat 30  31 

Title : Sharing and Groundness Dependencies in Logic Programs
Speaker : Harald Sondergaard, University of Melbourne
Time and Place : 11H00, Salle AURIGNY
Abstract :
We investigate Jacobs and Langen's Sharing domain, introduced for the analysis of variable sharing in logic programs, and show that it is isomorphic to Marriott and Sondergaard's Pos domain, introduced for the analysis of groundness dependencies. Our key idea is to view the sets of variables in a Sharing domain element as the models of a corresponding Boolean function. This leads to a recasting of sharing analysis in terms of the property of "not being affected by the binding of a single variable." Such an "unaffectedness dependency" analysis has close connections with groundness dependency analysis using positive Boolean functions. This new view improves our understanding of sharing analysis, and leads to an elegant expression of its combination with groundness dependency analysis based on the reduced product of Sharing and Pos. It also opens up new avenues for the efficient implementation of sharing analysis, for example using reduced order binary decision diagrams, as well as efficient implementation of the reduced product, using domain factorizations.

Title : Apercu de Coq - une application : preuve d'une mise en oeuvre de Java Card
Speaker : Gaëlle Segouat
Time and Place : 13H00, Salle AURIGNY
Abstract :
Afin d'utiliser la technologie Java sur les cartes a puce, un sous-ensemble de Java a ete defini : Java Card. Il s'agit de convertir le format Class File du bytecode Java en format CAP File accepte par une machine virtuelle Java Card. Ewen Denney a mis en place un cadre pour prouver la correction d'un convertisseur de Class File en CAP File. Nous formalisons son travail grace a l'assistant de preuve Coq, et prouvons qu'un certain ensemble de contraintes sur ce convertisseur suffit a en assurer la correction. Nous presentons ici l'assistant de preuve Coq, ainsi que le travail effectue pour formaliser en Coq la preuve de correction d'une mise en oeuvre de Java Card.

Retour en haut de la page
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Novembre 99
 
 
lundi  mardi  mercredi  jeudi vendredi  samedi  dimanche 
1  2  3  4  5 Sébastien Ferré
Séminaire Irisa : Marc Dymetman		 6  7 
8  9  10  11  12 Pont 13  14 
15  16  17  18  19 Thomas Colcombet 20  21 
22  23  24  25  26 Thèse de Sarah Mallet 27  28 
29  30 

Title : Systèmes d'information logiques.
Speaker : Sébastien Ferré
Time and Place : 13H00, Salle AURIGNY
Abstract :
Certains systèmes d'informations, tels que les systèmes de fichiers, utilisent une structure de navigation figée dans le sens où elle impose un certain ordre sur les critères de recherche et n'offre pas un langage de requêtes très expressif. Cette structure favorise ainsi certains types d'utilisation au détriment des autres, or il est courant qu'un système d'information soit utilisé par des utilisateurs divers avec des besoins différents. D'autres systèmes d'information, tels que les bases de données relationnelles, offrent un langage de requetes plus expressif, mais donne des réponses non structurées et difficilement exploitables (ex. réponses des moteurs de recherche sur le Web). Ce qui manque ici, c'est un système de navigation qui puisse guider progressivement l'utilisateur vers la réponse cherchée. Le problème est donc de concilier interrogation et navigation, tout en évitant les inconvénient des systèmes hybrides qui ont déjà été proposés. Le principe retenu est d'étiqueter les objets du système d'information par des formules logiques, puis d'utiliser l'analyse de concepts formels (ACF) pour définir une structure d'organisation et de navigation. Pour celà, l'ACF a tout d'abord été généralisée d'une logique simple à attributs vers une logique presque arbitraire. Puis un système d'information de type shell Unix a été réalisé pour une logique arbitraire : le shell conceptuel. Celui-ci a été instancié pour la logique à attributs de l'ACF et a permis d'effectuer quelques expérimentations. Les perspectives applicatives concernent les systèmes de fichiers, le génie logiciel et les applications grand public (ex. catalogues, guides touristiques).

Title :Automates d'arbres.
Speaker : Thomas Colcombet
Time and Place : 13H00, Salle AURIGNY
Abstract :
Les logiques temporelles permettent d'exprimer des contraintes sur le comportement de logiciels, de protocoles ou de circuits intégrés. On peut décrire dans ce formalisme une partie des spécifications d'un programme. Un outil (model-checker) est alors capable de vérifier automatiquement si un programme (ou plus exactement une abstraction d'un programme) vérifie ou non les spécifications.
Une telle vérification passe par la traduction de la formule logique et de l'abstraction du programme en un automate. Aux différents 'niveaux' de logiques temporelles (CTL, LTL, CTL*, mu-calcul) correspondent différents types d'automates (de mots infinis, d'arbres, alternants, hésitants...). Cette approche unique de la logique temporelle permet une étude précise de la complexité des problèmes de model-checking.
Nous présenterons le formalisme des automates d'arbres tout en montrant son lien avec les logiques temporelles. Nous décrirons alors le problème des conditions d'arrêt. Enfin nous montrerons comment les propriétés de certaines logiques peuvent être traduites en propriétés sur les automates, et comment en déduire des algorithmes de model-checking efficaces.
References :
@Article{Bernholtz:1994:ATA,

}
Version ps

@Article{Vardi:1996:ATA,

}
Version ps

@InCollection{00000234,

}

Title : Thèse : "Explications pour les bases de données déductives : associer trace et sémantique"
Speaker : Sarah Mallet
Time and Place : 11H00, salle Métivier
Abstract :
Une base de données déductive est une base de données interrogée à l'aide de programmes logiques. Ces programmes logiques sont écrits par des développeurs. Ils sont ensuite utilisés par des utilisateurs pour consulter la base de données. Développeurs et utilisateurs ont besoin de comprendre l'exécution des programmes qu'ils écrivent, pour les premiers, et qu'ils manipulent, pour les seconds. Ils n'ont pas la même vision de l'exécution d'un programme, les explications de l'exécution qui leur sont proposées doivent être différentes. Nous proposons une technique qui permet de définir des explications adaptables à l'utilisateur à partir d'un système de bases de données déductives existant. Cette technique s'appuie sur une trace de l'exécution déjà intégrée au système au moment de sa conception, nous évitons ainsi des modifications du système. Cette trace, qui reflète le niveau de l'implémentation, contient de l'information intéressante mais elle n'est compréhensible que par les implémenteurs. Il faut rendre la trace accessible à d'autres types utilisateurs. Pour cela, nous l'associons à une sémantique opérationnelle définie suivant des critères de cohérence, de monotonicité et de couverture mutuelle. Un prototype implémente cette association par un méta-interprète piloté par la trace. Les informations contenues dans la trace dirigent le méta-interprète et évitent de refaire des calculs effectués au cours de l'exécution, en particulier les accès à la base de données. Enfin, en utilisant des techniques d'instrumentation de méta-interprète, nous illustrons la flexibilité de notre technique pour définir des images de l'exécution.

Retour en haut de la page
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Décembre 99
 
 
lundi  mardi  mercredi  jeudi  vendredi  samedi  dimanche 
1  2  3 Séminaire Irisa : Les systèmes d'information mobiles 4  5 
6  7  8  9  10  Thomas Colcombet 11  12 
13  14  15  16  17  Tour de table 18  19 
20 Soutenance d'HDR (Thomas Jensen) 21  22  23  24  Noël 25  26 
27  28  29  30  31  Nouvelle année

Title : tissage de politiques de securite
Speaker : Thomas Colcombet
Time and Place : 13H00, salle Aurigny
Abstract : We propose an automatic method to enforce trace properties on programs. The programmer specifies the property separately from the program; a program transformer takes the program and the property and automatically produces another ``equivalent'' program satisfying the property. This separation of concerns makes the program easier to develop and maintain. Our approach is both static and dynamic. It integrates static analyses in order to avoid useless transformations. On the other hand, it never rejects programs but adds dynamic checks when necessary. An important challenge is to make this dynamic enforcement as inexpensive as possible. The most obvious application domain is the enforcement of security policies. In particular, a potential use of the method is the securization of mobile code upon receipt.

Les transparents de l'exposé Version ps
L'article présenté à POPL Version ps

Title : Analyse statique de programmes : fondements et applications
Speaker : Thomas Jensen
Time and Place : 10H00, salle Michel Métivier
Abstract : L'analyse statique regroupe une gamme de méthodes pour déterminer des propriétés du comportement d'un programme sans l'exécuter. Dans cet exposé je présenterai mes travaux concernant la spécification d'analyses statiques par des systèmes d'inférences (systèmes de types non-standards). D'abord je formaliserai le lien entre les systèmes de type et l'interprétation abstraite classique. Ensuite je montrerai comment cette approche s'applique aux différents domaines de programmation : l'analyse de nécessite pour des langages fonctionnels, l'analyse de relations entre variables dans des programmes synchrones et la vérification de propriétés de sécurité de programmes Java.

Retour en haut de la page
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Janvier 00
 
 
lundi  mardi  mercredi  jeudi  vendredi  samedi  dimanche 
1  2 
3  4  5  6  Séminaire Lande 7  Séminaire Lande 8  9 
10  11 Patrick Cousot 12  13  14  15  16 
17  18  19  20  21 Erwan 22  23
24  25  26  27  28 Fausto 29  30 
31 

Titre:Interprétation abstraite temporelle
Orateur: Patrick Cousot, Département Informatique, École Normale Supérieure, Paris
Heure et place: 14H00, salle Métivier
Résumé: Nous étudions l'interprétation abstraite de logiques et calculs temporels dans un cadre général, indépendant de la syntaxe, de la sémantique et des abstractions utilisées. Ceci est appliqué à un nouveau calcul temporel qui généralise le µ-calcul grâce à de nouvelles modalités d'abstraction existentielle et universelle et de renversement du temps ainsi qu'à une nouvelle sémantique de traces avec temps discret symétrique. La sémantique plus classique basée sur des ensembles d'états est une interprétation abstraite de cette sémantique de traces, qui est en fait incomplète, ce qui conduit à comprendre, de manière surprenante, la vérification de modèle (model-checking) et son application à l'analyse statique booléenne (dataflow analysis) comme des interprétations abstraites correctes mais en général incomplètes, même dans le cas de systèmes finis. Ceci conduit à étudier des sous-calculs et logiques complètes (comme c'est le cas pour CTL, mais pas pour CTL*).
 
 

Titre : Spécifier des modèles de traces en utilisant une sémantique par continuations.
Orateur: Erwan Jahier
Heure et place: 13H30, salle Oléron
 

Titre : Non Pair-Sharing and Freeness Analysis through Linear Refinement
Orateur: Fausto Spoto
Heure et place: 13H30, salle Oléron

Retour en haut de la page
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Février 00
 
 
lundi  mardi  mercredi  jeudi  vendredi  samedi  dimanche 
1  2  3  4  Jan Smaus 5  6 
7  8  9  10  11 Jean-François Boulicaut 12  13 
14  15  16  17  18 Jean-Philippe 19  20 
21  22  23  24  25 Tour de table 26  27 
28  29 
Titre : Bases de données inductives pour l'extraction de règles depuis des données binaires.
Orateur: Jean-François Boulicaut
Heure and Place : 13H30, salle Aurigny
Résumé : L'extraction d'ensembles fréquents dans des données binaires (n attributs booléens) est un des thèmes de recherche très actif en fouille de données (traduction française de "data mining"). A partir de telles propriétés, on induit facilement des règles conjonctives du type "Si A et B sont souvent vrais alors C et D le sont aussi et dans les mêmes tuples". On présentera le domaine de l'extraction de telles règles (appelées règles d'association) en insistant sur les possibilités d'extension les plus significatives, notamment celles qui reposent sur la notion de requête datalog fréquente (programmation logique inductive). Nous présenterons alors les travaux menés dans notre projet "Fouille de règles et bases de données généralisées" avec la collaboration de A. Bykowski et C. Rigotti.


Orateur : Jan Smaus
Heure et Place : 13H00, salle Oléron
Résumé: A class of predicates is identified for which termination does not depend on left-to-right execution. The only assumption about the selection rule is that derivations are input-consuming, that is, in each derivation step, the input arguments of the selected atom do not become instantiated. This assumption is a natural abstraction of previous work on programs with delay declarations. The method for showing that a predicate is in that class is based on level mappings, closely following the traditional approach for LD-derivations. Programs are assumed to be well and nicely moded, which are two widely used concepts for verification. Many predicates terminate under such weak assumptions. Knowing these predicates is useful even for programs where not all predicates have this property.
 
 

Titre Etude bibliographique sur les systèmes de détection d'intrusions
Orateur Jean-Philippe Pouzol
Heure et place 13H30, salle Oléron
Résumé Suite aux exposés de Véronique Abily et Mireille Ducassé lors du Grand Séminaire Lande du mois de janvier, je me propose de vous présenter un panorama des différentes approches décrites dans la littérature pous mettre en oeuvre des systèmes de détection d'intrusions dans les systèmes informatiques.
Après un très bref rappel sur les enjeux relatifs à la détection d'intrusions, je présenterai successivement : les approches basées sur une modélisation du comportement normal du système ; les approches basées sur la recherche de signatures d'attaques connues ; et enfin les travaux visant à distribuer la détection d'intrusions sur un réseau de machines.
La bibliographie est disponible en version .ps.gz.
Les transparents de l'exposé sont disponibles en version .ppt.gz

Retour en haut de la page
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Mars 00
 
 
lundi  mardi  mercredi  jeudi  vendredi  samedi  dimanche 
1  2  3 Frédéric Prost 4  5 
6  7  8  9  10 Lakshmi 11  12 
13  14  15  16  17 Séminaire Irisa : Gautam Biswas 18  19 
20  21  22  23  24  Siegfried 13h15
Meta, PVS 14h00		 25  26 
27  28  29  30  31  Pierre-Etienne Moreau
Titre : Dépendances de Typage
Orateur: Frédéric Prost
Heure and Place : 13H30, salle Aurigny
Résumé : Les d\'ependances d'un $\lambda$-terme sont (en gros) les parties de ce $\lambda$-terme qui contribuent au r\'esultat de son \'evaluation. Le probl\`eme de l'analyse des d\'ependances dans le $\lambda$-calcul pur a d\'ej\`a \'et\'e trait\'e. Cependant la m\'ethode n'est pas statique, il faut \'evaluer le terme jusqu'\`a sa forme normale pour d\'eterminer les sous-termes qui n'interf\`erent pas avec le terme global. Une technique (l'\'elagage) a \'et\'e propos\'ee pour r\'esoudre de mani\`ere statique une approximation de ce probl\`eme. Cette technique utilise le typage pour analyser les $\lambda$-termes. En fait, de nombreuses analyses reposent sur des propri\'et\'es du type non-interf\'erence, et utilisent le typage. Le plus souvent les syst\`emes consid\'er\'es sont des langage du premier ordre dans lesquels on ajoute des annotations aux types. Nous discuterons des points communs des diff\'erents syst\`emes propos\'es dans la litt\'erature, ainsi que des probl\`emes r\'ecurrents qu'ils rencontrent. Nous pr\'esenterons un calcul de d\'ependances pour le syst\`eme $F$ et montrerons une s\'emantique de ce calcul. Cette s\'emantique bas\'ee sur les relations d'\'equivalences partielles met en \'evidence les liens entre l'interpr\'etation abstraite et les analyses basees sur le typage.

Titre : TriSL: A Software Architecture Description Language and Environment
Orateur: Renganarayanan Lakshminarayanan
Heure and Place : 13H30, salle Aurigny
Résumé : As the size and complexity of a software system increases, the design problem goes beyond the algorithms and data structures of the computation. Designing and specifying the overall system structure -- or software architecture -- becomes the central problem. A system's architecture provides a model of the system that hides implementation detail, allowing the architect to concentrate on the analyses and decisions that are most crucial to structuring the system to satisfy its requirements. Unfortunately, with few exceptions, current exploitation of software architecture and architectural style is informal and ad hoc. The lack of an explicit, independent characterization of architecture and architectural style significantly limits the extent to which software architecture can be exploited using current practices. Architecture Description Languages(ADL) result from a linguistic approach to the formal description of software architectures. ADLs should facilitate building of architectures, not just specification. Further, they should also address the compositionality, substitutability, and reusability issues, which are the key to successful large-scale software development. A software architecture description language with a well defined type system can facilitate compositionality, substitutability, and reusability, the three keys to successful large-scale software development. Our contribution is a new software architecture description language, TriSL, which supports these features. In this talk we describe the design and implementation of TriSL. We demonstrate the power of our language and its expressiveness through case studies of real world applications.

Titre : Analyzing non-functional properties of mobile agents
Orateur: Siegfried
Heure and Place : ATTENTION 13H15, salle Aurigny
Résumé : The mobile agent technology is emerging as a useful new way of building large distributed systems. The advantages of mobile agents over the traditional client-server model are mainly non-functional. We believe that one of the reasons preventing the wide-spread use of mobile agents is that non-functional properties are not easily grasped by system designers. Selecting the right interactions to implement complex services is therefore a tricky task. We tackle this problem by considering efficiency and security criteria. We propose a language-based framework for the specification and implementation of complex services built from interactions with primitive services. Mobile agents, Rpc, remote evaluation, or any combination of these forms of interaction can be expressed in this framework. We show how to analyze (i.e. assess and compare) complex service implementations with respect to efficiency and security properties. This analysis provides guidelines to service designers, enabling them to systematically select and combine different types of protocols for the effective realization of interactions with primitive services.

Titre : PVS : utilisation du prouveur PVS pour la vérification de programmes réactifs
Orateur: Vlad Rusu, chargé de recherche à l'INRIA (mailto:Vlad.Rusu@irisa.fr)
Heure and Place :14H00, salle Jersey
Résumé : Le prouveur PVS est un outil qui permet d'automatiser en partie le raisonnement déductif. PVS est utilisé dans environ 200 universités et centres de recherche et commence à être utilisé dans l'industrie. Ses applications vont de la vérification de matériel aux preuves de théorèmes d'analyse mathématique.

Les atouts de PVS sont le langage de spécification, simple et puissant, ainsi que les procédures de décision intégrées aux commandes de preuve. Ces dernières évitent à l'utilisateur d'être encombré par les détails insignifiants de la preuve, lui permettant de se concentrer sur l'essentiel.

Dans ce cours-conférence, je présenterai, par l'intermédiaire d'exemples, le langage de spécification, le contrôle de types, ainsi que les principales commandes de preuve. Je donnerai un exemple de vérification de programmes avec PVS, en utilisant une combinaison de méthodes déductives, abstraction et model-checking.

Titre : Compilation de regles de reecriture et de strategies non-deterministes
Orateur: Pierre-Etienne MOREAU
Heure and Place : 13H30, salle Aurigny
Résumé : Les techniques de réécriture ont été développées depuis les années 1970 et appliquées en particulier au prototypage des spécifications formelles algébriques et à la démonstration de propriétés liées à la vérification de programmes.

ELAN est un système qui permet de spécifier et d'exécuter des résolveurs de contraintes, des démonstrateurs et plus généralement tout processus décrit par des règles de transformation. Il possède des opérateurs associatifs-commutatifs (AC) et un langage de stratégies qui permettent une gestion fine de l'exploration d'un arbre de recherche et une manipulation aisée de multi-ensembles et d'opérateurs mathématiques tels que les connecteurs booléens, les opérateurs arithmétiques ou les opérateurs de composition parallèle par exemple.

Ces deux notions améliorent grandement l'expressivité du langage mais introduisent un double non-déterminisme lié à la possibilité d'appliquer plusieurs règles, de différentes façons, sur un terme donné. Cela rend difficile et généralement peu efficace leur implantation.

L'objectif principal de ce travail est d'étudier des techniques de compilation qui améliorent l'efficacité de ce type de langages. Nous proposons un nouvel algorithme, à base d'automates déterministes, pour compiler efficacement le filtrage syntaxique. Nous définissons ensuite différentes classes de règles pour lesquelles nous proposons un algorithme efficace de filtrage AC. Cet algorithme utilise une structure de données compacte et les automates définis précédemment, ce qui améliore considérablement les performances du processus de normalisation dans son ensemble.

L'étude du langage de stratégies conduit à implanter des primitives originales de gestion du backtracking et à définir un algorithme d'analyse du déterminisme permettant de réduire leur usage et d'améliorer encore les performances, tout en réduisant l'espace mémoire nécessaire. Enfin, l'implantation des méthodes proposées a donné lieu à l'élaboration de nombreuses optimisations théoriques et techniques qui peuvent être largement réutilisées pour implanter d'autres langages de programmation par réécriture.

Dans le cadre de ce séminaire, je présenterai les algorithmes de compilation, l'architecture et le fonctionnement du compilateur, ainsi qu'une proposition d'environnement de spécification, fondée sur l'utilisation d'un format intermédiaire. Ce format intermédaire devrait permettre à terme de représenter les programmes et les calculs effectués. Ceci, dans l'optique de modulariser l'environnement tout en permettant d'effectuer des transformations de programmes et des analyses de traces.
 

Retour en haut de la page
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Avril 00
 
 
lundi  mardi  mercredi  jeudi  vendredi  samedi  dimanche 
1  2 
3  4 Sandrine Chirokoff 5 Olivier Danvy 6 7  Séminaire Irisa : Miroslav Malek 8  9 
10  11  12  13  14  Tour de Table 15  16 
17  18  19  20  21 Vacances  22  23 
24  25  26  27  28  Michael 29  30 

Titre :Une approche uniforme à la spécialisation de programmes et à la spécialisation de données
Orateur:Sandrine Chirokoff
Heure and Place : 14H00, salle Métivier
Résumé : Le développement de logiciels doit concilier deux propriétés importantes et contradictoires : généricité et performance. Pour résoudre ce problème, une approche prometteuse consiste à utiliser différentes techniques de spécialisation pour optimiser un programme générique en fonction d'un contexte d'utilisation donnée.

Toutefois, le degré de spécialisation d'un programme repose en grande partie sur les analyses qui identifient les calculs dépendant du contexte d'utilisation. Ces analyses, lorsqu'elles traitent un langage de taille réelle tel que C, demandent un effort de développement considérable et requièrent une mise au point délicate. Cette situation constitue un frein à l'exploration des différentes techniques de spécialisation puisque ces techniques ont jusqu'à maintenant été étudiées isolément. Ainsi, on constate que la spécialisation de programmes et la spécialisation de données ont toujours été traitées séparément. Bien que les transformations de programmes effectuées par ces deux stratégies soient différentes, l'identification des calculs invariants est un objectif commun. Cet aspect suggère que les analyses préparant la phase de transformations pourraient faire l'objet de diverses factorisations.

Dans cette thèse, nous formalisons les analyses de la spécialisation de données dans le but d'uniformiser cette méthode avec le spécialiseur de programmes Tempo. Ce travail permet, d'une part, l'intégration des analyses nécessaires à la spécialisation de données, et, d'autre part, la factorisation des développements de ces analyses. Nous montrons enfin que ce nouveau type de spécialiseur fournit au programmeur les stratégies complémentaires qui élargissent la portée de la spécialisation. Nous illustrons les avantages et les limitations de ces stratégies et leur combinaison sur une variété de programmes. Nous en concluons que la combinaison de ces deux techniques permet de traiter efficacement l'éventail des opportunités présentes dans un même programme.
 

Titre : Formalizing Implementation Strategies for First-Class Continuations
Orateur: Olivier Danvy
Heure and Place : 14H00, salle Métivier
Résumé : We present the first formalization of implementation strategies for first-class continuations. The formalization hinges on abstract machines for continuation-passing style (CPS) programs with a special treatment for the current continuation, accounting for the essence of first-class continuations. These abstract machines are proven equivalent to a standard, substitution-based abstract machine. The proof techniques work uniformly for various representations of continuations. As a byproduct, we also present a formal proof of the two folklore theorems that one continuation identifier is enough for second-class continuations and that second-class continuations are stackable.

To be presented at ESOP'00.
 

Titre : Séminaire Irisa : Delivering Dependability and Speed to Web Users
Orateur: Miroslav Malek
Heure and Place : 14H00, salle Jersey
Résumé :

As the web revolutionizes the modus vivendi and the modus operandi of the human race with continuously changing technologies and business models, dependability, speed, and security will be of an essence. You will be taken on a short journey of the past, the present and the future of the web followed by a brief overview of omniscience, consensus and autonomy paradigms and their suitability to the web environments. Most of the dependable, real-time systems to date have been implemented in embedded settings and there is an urgent need to open up this type of computing technology to a larger number of users utilizing heterogeneous web environments. State-of-the-art commercial off-the-shelf (COTS) systems concentrate mostly on optimizing performance, neglecting the importance of predictable end-to-end service availability.

The talk will present our approach to responsive cluster computing, i.e., the delivery of predictable, timely services even in the presence of faults. Our major projects focus on foundations, specification, design and implementation of basic concepts and protocols for support of predictable, high performance responsive computing. We have developed a consensus-based approach to fault-tolerant computing and investigated responsiveness tradeoffs between checkpointing and replication. Additional research considers scheduling policies which support dependability and timeliness in high performance environments. Reliability, (re-) configuration as well as QoS adaptation for the pure video/data transmission will be described in the context of teleteaching and tele-laboratory scenarios, which can tolerate certain classes of faults including fault tolerant browsers.

A concept of "Composite Objects" as a filtering bridge between standard middleware platforms and software frameworks providing predictable services with certain quality-of-service (QoS) guarantees will be presented. Results focus on fault-tolerant real-time computing utilizing the CORBA middleware platform and can be applied to, e.g., process-control and robotics. A software tool generating fault-tolerant services will also be outlined.

Retour en haut de la page
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Mai 00
 
 
lundi  mardi  mercredi  jeudi  vendredi  samedi  dimanche 
1  2  3  4  5  6  7 
8  9  10  11  12   Henrik Nilsson 13  14 
15  16  17  18  19 David 20  21 
22 Jean-Christophe Filliatre 23  24 Carlton Pu 25  26  Tour de Table 27  28
29  30  31 

Titre : How to Look Busy while Being as Lazy as Ever: The Implementation of a Lazy Functional Debugger
Orateur: Henrik Nilsson
Heure and Place : 13H30, salle Aurigny
Résumé : In this talk, I'll describe the implementation of a debugger for lazy functional languages like Haskell. The key idea is to construct a declarative trace which hides the operational details of lazy evaluation. However, to be useful, the scheme must not be too expensive in terms of time and space for tracing. Thus, to avoid excessive memory consumption (and the time overhead of constructing parts of the trace that will never be inspected), the trace is constructed one piece at a time, as needed during a debugging session, by automatic re-execution of the program being debugged. In the talk, I'll cover both the underlying ideas and some of the central points of the implementation. Performance figures will also be presented which shows that the approach is fairly efficient.
 

Titre : Formalization and Verification of Coherence Protocols with the Gamma Framework
Orateur: David Mentré
Heure and Place : 13H30, salle Aurigny
Résumé : Je présenterais un algorithme de vérification automatique de protocoles de cohérence utilisés dans les mémoires virtuelles partagées. Pour ce faire, les protocoles sont représentés par une variante du formalisme Gamma, c'est à dire par des règles de réécritures sur des multi-ensembles. L'état global du protocole est représenté par un multi-ensemble et les changements d'états sont représentés par les règles de réécriture. Les invariants sont exprimés par des propriétés sur la cardinalité de sous-ensembles qui caractérisent certaines relations spécifiques (celui qui a compris cette phrase me le dit ;-). Notre algorithme vérifie qu'une propriété est un invariant du protocole. Je montrerais également quelques résultats préliminaires et comparerais notre approche avec deux autres méthodes couramment utilisées.
 

Titre : Preuve de programmes impératifs en théorie des types
Orateur: Jean-Christophe Filliatre
Heure and Place : 14H00, salle Aurigny
Résumé : Nous étudions le problème de la certification de programmes mêlant traits impératifs et fonctionnels dans le cadre de la théorie des types.

La théorie des types constitue un puissant langage de spécification, naturellement adapté à la preuve de programmes purement fonctionnels. Pour y certifier également des programmes impératifs, nous commençons par exprimer leur sémantique de manière purement fonctionnelle. Cette traduction repose sur une analyse statique des effets de bord des programmes, et sur l'utilisation de la notion de monade, notion que nous raffinons en l'associant à la notion d'effet de manière générale. Nous montrons que cette traduction est sémantiquement correcte.

Puis, à partir d'un programme annoté, nous construisons une preuve de sa spécification, traduite de manière fonctionnelle. Cette preuve est bâtie sur la traduction fonctionnelle précédemment introduite. Elle est presque toujours incomplète, les parties manquantes étant autant d'obligations de preuve qui seront laissées à la charge de l'utilisateur. Nous montrons que la validité de ces obligations entraîne la correction totale du programme.

Nous avons implanté notre travail dans l'assistant de preuve Coq, avec lequel il est dès à présent distribué. Cette implantation se présente sous la forme d'une tactique prenant en argument un programme annoté et engendrant les obligations de preuve. Plusieurs algorithmes non triviaux ont été certifiés à l'aide de cet outil (Find, Quicksort, Heapsort, algorithme de Knuth-Morris-Pratt).
 

Titre : INFOSPHERE: SMART DELIVERY OF FRESH INFORMATION
Orateur: Calton Pu
Heure and Place : 11H00, salle Métivier
Résumé : While huge amounts of information pervade our environment, it has been difficult to filter it and bring it to humans in a clean, reliable, and timely way. This fast growing information jungle needs to be tamed and civilized, to become a nurturing Infosphere in which the Information Age will flourish. Our vision of a civilized Infosphere goes beyond just gathering, storing, and retrieving increasing amounts of information. Living in the Infosphere means being in constant contact with both the physical world and the information civilization. In general, the Infosphere supplies fresh information that changes the way we interact with our environment. An accurate weather forecast could mean a happy birthday party in the park for kids, saving a crop or bankruptcy for farmers, or a matter of life or death for a military operation in hostile territory. Similarly, having an accurate picture of the highway conditions may mean arriving at work on time, beating the deadline for an important delivery, or reaching the hospital before the patient dies. We envision the Infosphere providing more details about the current state of our physical world than ever imaginable, impartially to all human beings. We believe that the missing link in the construction of Infosphere is the software to manage information flow from the information producers to consumers. We propose the Infopipe abstraction to link information producers to consumers. In addition to their basic function of transporting information, Infopipes manage and manipulate the concrete delivery properties of the information flowing through them, such as freshness. Infopipe creation and composition involve the specification of these properties and system resource management mechanisms to maintain them. The property specifications are translated automatically by the system into an actual implementation with the desired behavior. When information flows through an Infopipe, concrete delivery properties and requirements such as freshness, performance, and security are updated en route and maintained each step of the way. The three components of Infopipe, the property management, the feedback-based resource management, and the smart information delivery, can be combined to form an Infosphere that brings the right information to the right user at the right time.

Retour en haut de la page
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Juin 00
 
 
lundi  mardi  mercredi  jeudi  vendredi  samedi  dimanche 
1  2 Pont 3  4 
5  6  7  8  9 Sébastien 10  11 
12  13  14  15  16 Romain Guider 17  18 
19  20  21  22  23 Tour de table 24  25
26  27  28  29  30 Thomas Colcombet

Titre: Analyse de concepts formels
Orateur : Sébastien Ferré
Heure et place : 13h30 salle Aurigny
Résumé : L'analyse de concepts formels (ACF) trouve ses fondements dans la théorie des treillis (Birkhof 40)
et apparaît dans le domaine de l'informatique au début des années 80 (Wille 82). Elle propose une
formalisation des notions de contexte et de concept et fut d'abord appliqué dans le domaine de l'analyse
de données. Bien que celle-ci reste le domaine privilégié de l'ACF, on trouve aussi des applications en datamining,
en apprentissage, dans les systèmes d'information, et le domaine d'application de l'ACF ne cesse de s'étendre.
Pour répondre à la diversité de ces applications, diverses extensions de l'ACF ont été proposées mais aucune ne
couvre tous les besoins présents et à venir.
Nous proposons une généralisation logique de l'analyse de concepts, l'Analyse de Concepts Logique (ACL), qui
subsume toutes les extensions connues et qui permet de décrire les données traitées par une logique (presque)
arbitraire. Nous montrons en particulier qu'un contexte logique induit une logique "contextualisée" qui offre
un cadre commun aux diverses applications de l'ACF. Nous nous intéressons plus particulièrement à son application
aux systèmes d'information logiques.
Cet exposé est de nature introductive et s'attachera à l'explication des notions élémentaires et à la présentation
des diverses applications.

Titre: Analyse statique de programmes Java, application à la parallélisation
Orateur : Romain Guider
Heure et place : 13h30 salle Aurigny
Résumé : Nous présentons dans ce travail une analyse statique de programmes à objets par interprétation abstraite. L'analyse de programmes à objets comporte deux particularités que nous traitons séparément : l'analyse du flot de contrôle et la représentation des graphes d'objets. Dans un premier temps, nous présentons une analyse de flot de contrôle paramétrée par une représentation abstraite des graphes d'objets. Cette analyse est générique et peut servir de base à de nombreuses applications.

Nous dérivons de notre interpréteur abstrait une présentation des problèmes d'analyse statique sous la forme d'un système d'équations. La présentation sous cette forme permet d'une part de résoudre efficacement les problèmes d'analyse en utilisant des stratégies d'itérations de point fixe sophistiquées. De plus, le mode de construction du système d'équations (opérateur de point fixe) nous permet d'envisager des applications {\it non standard}.

Dans un second temps nous instancions notre analyseur statique en utilisant un domaine abstrait pour les graphes d'objets qui est dû à Sagiv, Reps et Wilhelm. Nous étendons ce domaine pour construire une analyse interprocédurale et nous l'augmentons d'une opération de ramasse miette abstrait qui permet d'analyser avec précision des opérations telles que la suppression d'un élément d'une liste chaînée (l'analyse est capable de détecter qu'une liste chaînée après une opération de suppression a encore la structure d'une liste chaînée). Nous décrivons également une technique, basée sur ce domaine abstrait, qui permet d'analyser des fragments de programmes.

Enfin, nous décrivons une application de l'analyse statique à la parallélisation et à la distribution de programmes à objets. Nous donnons un critère de parallélisation qui permet d'identifier les objets auxquels on peut attacher leur propre fil d'exécution tout en préservant la sémantique séquentielle. Nous interprétons ensuite ce critère sur les domaines abstraits, ce qui nous permet de les vérifier statiquement.

Pour finir, nous décrivons l'implantation que nous avons faites de notre analyse et nous présentons également des transformations de programmes qui permettent d'analyser plus facilement le byte code Java.

Titre:Treillis à complexité bornée
Orateur : Thomas Colcombet
Heure et place : 13h30 salle Aurigny
Résumé : La qualité d'une analyse de programme peut être caractérisée suivant deux critères : sa complexité et sa précision. Dans la théorie de l'interprétation abstraite (P.Cousot) les propriétés inférées par une analyse sont modélisées par un treillis. Dans ce cadre, la complexité d'une analyse est fortement corrélée à l'efficacité des opérateurs abstraits et à la profondeur du treillis choisi. La précision quant à elle peut s'identifier à la taille de ce treillis.

Mettre au point une bonne analyse de programme revient à trouver un compromis acceptable entre complexité et précision, c'est à dire choisir un treillis convenable.

La solution proposée habituellement en interprétation abstraite consiste à travailler sur un treillis plus grand que nécessaire et à utiliser un opérateur d'élargissement (widening) pour accélérer le calcul. Cet opérateur correspond toujours à une perte de précision non contrôlée (au mieux orientée approximativement par des heuristiques). Cette technique peut être vue comme une diminution *dynamique* de la complexité du treillis.

Dans cet exposé, je vous montrerai à travers deux exemples (un treillis d'anneaux de polynômes, et un treillis de formules logiques) que borner *statiquement* la complexité d'un treillis est une alternative intéressante au plus classique élargissement.



Retour en haut de la page
 
 
 
 

Exposés en attente