Serveur interne
Accès réservé
Accès réservé
|
|
|
|||
|
|
|
|
|
Serveur interne
Accès réservé |
|
|
|
|
|
|
| orateur
: |
Florence Charreteur |
| titre
: |
Amélioration du traitement des appels de fonctions dans InKa |
| résumé
: |
La génération automatique de cas de test vise à générer des entrées pour un programme sous test face à un objectif de test donné par le testeur. Le prototype InKa, développé depuis une dizaine d'années, permet la génération par contraintes de cas de test pour des programmes C complexes. Cependant, en cas d'appels de fonctions répétés, le temps de génération des cas de test peut croître rapidement, ce qui pose problème pour l'extension du prototype au test du C++. Une méthode d'accélération de la résolution du système de contraintes généré dans l'outil InKa en présence d'appels de fonctions sera présentée. Cette méthode se base sur des subdivisions du système de contraintes pour traiter les contraintes dans un ordre jugé plus optimal. Les résultats sont concluants, un gain de temps significatif est généralement observé. |
| orateur
: |
Étienne André |
| titre
: |
Mise en oeuvre et évaluation d'analyses modulaires de bytecode Java spécifiées avec Datalog |
| résumé
: |
Situé dans le cadre de l'analyse statique de classes, ce projet de fin d'études se propose d'analyser le bytecode Java à l'aide de contraintes Datalog. Les contraintes sont générées automatiquement à partir des instructions bytecode puis résolues, et on peut par la suite déduire des informations variées sur le programme, notamment les graphes d'appels ou diagrammes d'objets. En outre, cette analyse s'effectue de manière modulaire, c'est-à-dire que les classes peuvent être analysées indépendamment les unes des autres. Ceci devrait en particulier permettre des prétraitements sur les contraintes, afin de réduire leur temps de résolution. |
| où
et quand ? |
Salle Crète à
14h |
| orateur
: |
Christophe Alias (LIP) |
| titre
: |
Optimisation de programmes par reconnaissance de templates |
| résumé
: |
La plupart des optimisations appliquent des transformations locales
bas-niveau, sans se soucier du calcul exprimé par le programme. Bien que ces
optimisations produisent des résultats satisfaisants, elles ne se substituent
pas à un bon algorithme, et aménent bien souvent le programmeur à utiliser
des bibliothèques optimisées. Pour le moment, les bibliothèques optimisées
doivent être appelées à la main. Apprendre et utiliser une nouvelle
bibliothèque est malheureusement très fastidieux, et il est surprenant de
voir le peu d'aide apporté par le compilateur. Une solution naturelle serait
de chercher les occurrences des fonctions d'une bibliothèque dans le
programme, et de les remplacer par l'appel correspondant.
Dans cet exposé, nous présentons une approche totalement automatique pour
reconnaître dans un programme les occurrences des fonctions d'une
bibliothèque optimisée, et les substituer par l'appel de fonction
correspondant lorsque c'est possible et intéressant en terme de performances.
Notre approche a été implémentée dans l'outil TeMa (Template Matcher). TeMa
comporte plus de 17000 lignes de code C++ et OCaml, et a été appliqué à la
détection des fonctions de la bibliothèque BLAS (Basic Linear Algebra
Subroutines) dans les noyaux des benchmarks SpecFP 2000 et Perfect Club. Les
résultats expérimentaux montrent un facteur d'accélération substanciel sur
les noyaux swim, mgrid et mdg. MOTS-CLES
|
| où
et quand ? |
Salle Minquiers à
14h30 |
| orateur
: |
Arnaud Gotlieb |
| titre
: |
INKA V2 |
| résumé
: |
Ten years ago, we wrote a first paper on the use of constraint (logic) programming to automatically generate white-box test data for imperative programs. This work opened the road to several research and development projects on this topic and led us to the design of INKA a software test data generator for C/C++. Ten years later, where are we? This talk proposes to review the advances we made on constraint-based test data generation and details the architectural design of INKA V2 which is a state-of-the-art implementation of our research and development works. The talk will end by introducing current work we perform to extend the tool.
|
| où
et quand ? |
Salle Oléron à
15h |
| orateur
: |
Jean-Yves Moyen |
| titre
: |
Analyse de programmes et complexité implicite |
| résumé
: |
Je présenterai différentes techniques d'analyses de programmes en vu d'obtenir des bornes sur leur complexité. Ceci permet d'obtenir plusieurs caractérisations syntaxiques de classes de complexité usuelles comme Ptime ou Pspace. De plus, je mettrai l'accent sur les aspects de complexité implicite (complexité du programme comparée à la complexité de la fonction comparée) et d'intentionnalité (capturer le plus possible d'algorithmes "naturels" dans la caractérisation).
|
| où
et quand ? |
Salle Minquiers à
14h30 |
| orateur
: |
Frédéric Besson |
| titre
: |
A PCC Architecture based on Certified Abstract Interpretation |
| résumé
: |
Proof-Carrying Code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's security policy. We show how certified abstract interpretation can be used to build a PCC architecture where the code producer can produce program certificates automatically. Code consumers use proof checkers derived from certified analysers to check certificates. Proof checkers carry their own correctness proofs and accepting a new proof checker amounts to type checking the checker in Coq. Fixpoint compression techniques are used to obtain compact certificates. The PCC architecture has been evaluated experimentally on a byte code language for which we have designed an interval analysis that allows to generate certificates ascertaining that no array-out-of-bounds accesses will occur.
|
| où
et quand ? |
Salle Oléron à
14h30 |
| orateur
: |
Pascal Sotin |
| titre
: |
Quantitative Static Analysis over semirings: analysing cache behaviour for Java Card |
| résumé
: |
We present a semantics-based technique for modeling and analysing resource usage behaviour of programs written in a simple object oriented language like the Java Card byte code. The approach is based on the quantitative abstract interpretation framework of Di Piero and Wicklicky where programs are represented as linear operators. We consider in particular linear operators over semi-rings (such as max-plus) that have proven useful for analysing cost properties of discrete event systems. We illustrate our technique through a cache behaviour analysis for Java Card.
|
| où
et quand ? |
Salle Oléron à
14h30 |
| orateur
: |
Didier Le Botlan (EMN) |
| titre
: |
MLF : réconcilier ML et Système F |
| résumé
: |
Les langages de programmation comme OCaml et Haskell reposent sur des
règles de typage garantissant la bonne exécution des programmes. En
pratique, le typage permet de détecter maintes erreurs de programmation
à la compilation. Depuis vingt ans, de nombreux travaux visent à
enrichir ces systèmes de types avec le polymorphisme de première classe
(i.e. en ajoutant le quantificateur universel "pour tout"). Le
référentiel pour le polymorphisme a été défini en 1972 dans le domaine
de la logique : c'est le Système F (Girard). Mais en pratique, le
Système F est inutilisable comme langage de programmation, à la
différence de OCaml ou Haskell. De plus, l'adaptation naïve du Système F
à ces langages rend le typage indécidable.
Dans cet exposé, nous détaillons intuitivement le problème en expliquant
pourquoi les solutions proposées jusqu'à présent ne sont pas
satisfaisantes. Nous présentons ensuite MLF, un système de types qui
répond aux exigences posées, puis nous illustrons avec des graphes
l'algorithme d'unification de MLF.
|
| où
et quand ? |
Salle Oléron à
14h30 |
| orateurs
: |
Erwan Quesseveur, Arnaud Lepetit, Olivier Bedel |
| titre
: |
Présentation des activités géomatiques du laboratoire Reso (Université de Rennes 2) |
| résumé
: |
Le laboratoire Reso, spécialisé en géographie sociale, étudie les dynamiques sociales et spatiales des villes et des campagnes, ainsi que les politiques publiques et l'aménagement du territoire, à différentes échelles. Au sein du laboratoire, la cellule géomatique s'intéresse plus particulièrement à l'étude des phénomènes spatiaux au moyen d'outils et de méthodes d'analyse dédiés (basés sur les systèmes d'information géographique). Dans la première partie de l'exposé, nous introduirons ces outils de manipulation et d'analyse de l'information géographique. Nous détaillerons également la chaîne de valorisation que l'on peut construire autour de ces techniques : du stockage de la donnée géographique brute à la diffusion d'une information cartographique, en passant par des traitements spatiaux et statistiques, et/ou l'utilisation de modèles spécifiques. La seconde partie de l'exposé sera consacrée à la présentation de quelques projets réalisés ou en cours, autour des thématiques de la protection de lÕenvironnement, de la mobilité ou encore de la gestion de crise.
|
| où
et quand ? |
Salle Minquiers à
14h30 |
| orateur
: |
Xavier Rival (ENS) |
| titre
: |
Certification de programmes embarqués au niveau du code source et du code compilé |
| résumé
: |
Une erreur à l'exécution dans un programme embarqué, par exemple dans le
domaine de l'aéronautique, peut avoir des conséquences critiques. Par
conséquent, nous nous proposons d'étudier la certification d'absence
d'erreurs à l'exécution dans de tels programmes.
Dans une première partie, nous considérons le cas de programmes C, générés
à partir d'une spécification synchrone. Dans le cadre du projet Astrée
(ENS et Ecole Polytechnique), en collaboration avec Bruno Blanchet,
Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine
Miné et David Monniaux, nous avons mis au point un analyseur capable de
prouver automatique l'absence d'erreurs à l'exécution dans des programmes
réels de grande taille. Au cours de cette partie, nous décrirons la
structure de l'analyseur, ainsi que le domaine abstrait utilisé (algèbre
de propriétés intervenant dans l'inférence d'invariants numériques et
symboliques).
Dans une seconde partie, nous nous intéresserons à la certification des
mêmes programmes, après compilation. Plus précisément, nous considérerons
deux propriétés importantes à démontrer : l'absence d'erreur à l'exécution
et l'implémentation correcte des fonctions décrites dans le code source.
Pour cela, nous formalisons la compilation dans le cadre de
l'interprétation abstraite ainsi que des algorithmes de vérification
adaptés. En particulier, la technique de traduction d'invariants abstraits
permet d'utiliser les résultats d'une analyse du code source (par exemple,
utilisant Astrée) pour produire des invariants que l'on peut ensuite
traduire et vérifier au niveau assembleur. D'autre part, la technique de
preuve d'équivalence vérifie des conditions locales, qui assurent
l'équivalence d'une abstraction de la sémantique du programme compilé et
du programme source.
|
| où
et quand ? |
Salle Oléron à
14h30 |
| orateur
: |
Thomas Jensen |
| titre
: |
Analyse certifiée pour la sécurité du code mobile |
| résumé
: |
Je ferai un résumé des techniques de base de l'interpretation abstraite pour l'analyse du byte code Java et décrirai une architecture de "proof-carrying code" fondée sur la version certifiée de ces analyses.
|
| où
et quand ? |
Salle Bréhat à
14h30 |
| orateur
: |
Tristan Denmat |
| titre
: |
Amélioration de la détection d'insatisfiabilité dans Inka |
| résumé
: |
InKa est un outil de génération de cas de test qui utilise la programmation logique avec contraintes sur des domaines finis (CLP(FD)). Inka peut aussi être utilisé pour vérifier des propriétés numériques. Le principe est de transformer un programme impératif ainsi que la négation de la propriété en contraintes CLP(FD) et de montrer que le store de contraintes ainsi obtenu n'a pas de solutions (on dit alors qu'il est insatisfiable). Malheureusement, nous verrons pendant la première partie de l'exposé que CLPFD n'est pas très performant en ce qui concerne la détection d'insatisfiabilité. Un moyen de contrer ce problème est de se ramener à la détection d'insatisfiabilité d'un store de contraintes linéaires, qui est un problème décidable sur les rationnels. Nous présenterons donc deux points. D'une part comment générer une sur approximation linéaire d'un programme impératif. D'autre part comment faire coopérer CLPFD avec un solveur linéaire pour améliorer la détection d'insatisfiabilité.
|
| où
et quand ? |
Salle Oléron à
14h30 |
| orateur
: |
Matthieu Petit |
| titre
: |
Probabilistic Choice Operators as Constraints Combinators |
| résumé
: |
Dans cet exposé, je vais vous présenter les travaux effectués avec Arnaud depuis cet été. Notre travail porte sur une extension déclarative du langage PCCP (Probabilistic Concurrent Constraint Probabilistic). Considérer l'opérateur de choix probabiliste de PCCP comme un combinateur de contraintes nous permet de raisonner sur un choix probabiliste partiellement connu. Dans notre cadre, la connaissance partielle sur le choix probabiliste prend la forme de contraintes portant sur le domaine de variation et la distribution de probabilité d'une variable aléatoire.
Après une présentation rapide du cadre de travail, nous décrirons les nouvelles fonctionalités apportées à l'opérateur. Ensuite, l'algorithme de filtrage associé au combinateur de contraintes sera présenté. Nous discuterons pour finir du domaine d'application de ce travail (test statistique structurel).
|
| où
et quand ? |
Salle Minquiers à
14h30 |
| orateur
: |
Alexandre Pocquet (Laboratoire MACCLIA, CREC Saint-Cyr) |
| titre
: |
Réseaux Ad Hoc et Sécurité |
| résumé
: |
L'objet de cette présentation est d'établir un état de l'art sur les réseaux sans fils sans infrastructure appelés réseaux Ad Hoc en précisant leurs besoins spécifiques et les stratégies développées en terme de sécurité.
Les réseaux de communication intègrent de plus en plus notre quotidien, que ce soit dans le domaine privé ou le domaine professionnel. Leurs utilisations dans certains contextes ont mis en évidence des besoins spécifiques nécessitant des stratégies différentes.
Les réseaux Ad Hoc, contrairement à leurs homologues filaires, doivent répondrent en plus, à des besoins particuliers de mobilité, de couverture aérienne et de sécurité. Les stratégies déployées portent sur l'architecture du réseau, les mécanismes de routage de l'information et les protocoles de sécurité.
Les réseaux Ad Hoc ont pour vocation de fonctionner sans équipements fixes et dédiés, leurs fonctions essentielles ainsi que leur gestion sont assurées par une architecture entièrement répartie. Le support de transmission étant aérien, et par conséquent non protégé, la sécurité au sein des réseaux Ad Hoc nécessite de nouveaux modèles au regard des exigences sécuritaires classiques.
Nous commencerons par définir les réseaux Ad Hoc en explicitant leurs contraintes spécifiques en terme de mobilité et de sécurité et en détaillant les stratégies mises en oeuvre pour y remédier.
|
| où
et quand ? |
Salle Guernesey à
14h30 |
| orateur
: |
Sébastien Ferré |
| titre
: |
Logical Data-mining in the framework of Logical Information Systems |
| résumé
: |
Logical Information Systems (LIS) are founded on 2 theories: logic
functors and logical concept analysis. Logic functors enable us to
build ad-hoc complex logics from reusable components. Logical concept
analysis formalizes relationships between the logical properties and
the sets of objects of a data context. LIS were initially designed for
combining querying and navigation, but they also allow for various
data-mining tasks like concept learning or classification. A
specificity of LIS is that objects, queries, navigation links,
hypotheses, etc. are represented by the formulas of an almost
arbitrary logic, which helps to mine structured data compared to
propositional methods. As logics can be customized to each
application, it gives more flexibility in tuning the trade-off
expressivity/efficiency than in ILP. The customization of logics is
made accessible to non-logicians thanks to logic functors. LIS are now
mature for querying and navigation, and a few experiments have been
done in data-mining and machine learning.
|
| où
et quand ? |
Salle Guernesey à
14h30 |
| orateurs
: |
Olivier Bedel, Olivier Ridoux |
| invités
: |
Erwan Quesseveur (maître de conférences au RESO, laboratoire de géographie sociale de l'Université de Rennes 2) et François Leprince (chercheur associé au RESO et directeur associé de la société Alkante), qui ont tous deux participé à l'élaboration du projet GEOLIS Thomas Devogele, Maître de conférences, Groupe de recherche en SIG de l'École Navale (Lanveoc-Poulmic) |
| titre
: |
GEOLIS, un système d'information logique pour l'information géographique |
| résumé
: |
Nous présenterons dans cet exposé le projet GEOLIS qui constitue le
cadre de ma thèse et dont le principal défi est d'appliquer les
principes de navigation et d'interrogation des systèmes d'information
logiques à l'information géographique. Aujourd'hui, l'information
géographique est de plus en plus présente dans notre société, aussi
bien au niveau des professionnels et des institutions chargés de
l'administration d'un territoire (Communauté d'agglomération,
pompiers) que du grand public avec par exemple, les outils d'aide à la
navigation par GPS, ou les outils de visualisation comme Google
Earth. Les systèmes d'information géographique sont des outils dédiés
à la manipulation, l'analyse et la visualisation de cette information
présentant une composante géographique (représentation spatiale,
référencée dans un repère terrestre). Dans la premiere partie de
l'exposé, Olivier présentera les principes du système d'information
logique développé par le groupe LIS. Dans un second temps, je
présenterai brièvement les systèmes d'information géographique, en
introduisant leurs principales fonctions, les différents types de
données géographiques et l'architecture de ces systèmes. Je
détaillerai également une utilisation des SIG pour la modélisation des
écoulements de surface, thème sur lequel j'ai travaillé au sein du
laboratoire RESO. Enfin, nous discuterons avec nos invités des apports
d'une organisation et d'une exploitation logique des données
géographiques en termes de fouille de données et de gestion des niveaux
d'échelle.
|
| où
et quand ? |
Salle Bréhat à
14h30 |
| orateur
: |
Guillaume Dufay |
| titre
: |
Protection de la vie privée avec JML |
| résumé
: |
Nous décrirons dans cet exposé des travaux menés afin d'assurer des propriétés de protection de la vie privée d'algorithmes de fouille de données. Ces propriétés sur du code source Java sont exprimées dans le langage JML et vérifiées par les outils Krakatoa/Coq. Néanmoins les spécifications JML ne suffisent pas à énoncer des propriétés évoluées comme la non-interférence. Nous exposerons différentes classes de propriétés attendues pour la protection de la vie privée, montrerons informellement comment étendre JML et Krakatoa pour prendre en compte la non-interférence et discuterons des points à approfondir. |
| où
et quand ? |
Salle Bréhat à
14h30 |
| orateur
: |
Damiano Zanardini, Universita' di Verona |
| titre
: |
Abstract Non-Interference with Java classes |
| résumé
: |
The information flow
property of Non-Interference was recently relaxed into Abstract Non-Interference (ANI), where only properties of data can be observed by attackers. ANI was originally defined on integer values; properties identified sets of integers. An Object-Oriented reformulation of ANI is presented, in which data can belong to any classes. Abstract domains are represented in terms of class hierarchies: the upper closure operator representing the abstraction function maps an object into the smallest class containing it. An algorithm is provided, which checks dependencies between data: it computes which data can affect the class (abstract property) of variables and fields. A program is secure for a given domain if the output class of low security fields does not depend on the input class of high security fields. The analyzer uses Boolean functions for describing the information flow properties of programs. The correctness proof for the analyzer guarantees that no dangerous program can be accepted. |
| où
et quand ? |
Salle Oléron à
15h |
 |
|||
|
