Merci aux intervenants de communiquer à Ph. Schnoebelen toutes informations, précisions, corrections, ..., qui pourraient améliorer le contenu de cette page. En particulier, je serai ravi d'ajouter des liens vers vos homepages, ou vers un papier, des transparents, etc. qui reprendraient le thème de votre intervention.
Le programme complet est disponible.
Un résumé est disponible. Le PDF des transparents sera disponible sur le réseau après l'exposé.
FOC est un langage, dédié au calcul formel, qui permet d'une part , de déclarer et de définir des fonctions, d'autre part, d'exprimer les propriétés de ces fonctions et de les prouver. Ce langage possède des traits objets (héritage multiple, liaison retardée), une certaine forme de modularité et une possibilité de paramétrage assez étendue. L'utilisation conjointe de ces traits peut engendrer des incohérences au niveau logique. Le compilateur du langage effectue une analyse de cohérence. Il extrait ensuite les parties calculatoires du source et les compile vers Ocaml. De même, il extrait les parties logiques du source et les compile vers Coq. L'exposé contiendra une présentation générale du langage, mettant l'accent sur les aspects programmation et preuve.
Toute surface compacte orientable sans bord est, à homéomorphisme près, une sphère ou un g-tore (accolement de g tores, pour un g>0). Un système (fondamental) de lacets d'un g-tore est un ensemble de lacets simples ayant un point commun v, deux à deux disjoints sauf en v, tel que le découpage de la surface selon ces lacets donne un disque topologique. On sait calculer des systèmes de lacets d'une surface, ce qui est utile dans plusieurs applications (paramétrisation, maillage, plaquage de textures) ; mais il est souvent souhaitable d'avoir des lacets aussi courts que possible. Dans un cadre où les lacets sont tracés sur le graphe sommets-arêtes d'une surface triangulée, nous présentons un algorithme polynomial qui calcule un système de longueur minimale parmi tous les systèmes d'une classe d'homotopie donnée. Travail en collaboration avec Francis Lazarus, paru dans Proceedings of the 43rd IEEE Symposium on Foundations of Computer Science (FOCS'02), novembre 2002, pages 627-636.
Le photo-réalisme en synthèse d'images nécessite l'intervention de nombreux paramètres, ainsi que des calculs complexes. Le but peut être considéré comme atteint lorsque un observateur ne peut plus faire la différence entre une simulation et une photographie de la scène simulée. Pour atteindre cet objectif, il est nécessaire d'effectuer des calculs complexes, aussi bien au niveau de la géométrie de la scène, de la simulation des matériaux, ou encore de l'interaction lumière matière. Toutefois, un élément est souvent oublié dans cette quête de réalisme :\1l'environnement d'observation. Cette simulation est en effet observée sur un dispositif de visualisation, par un observateur humain, placé dans un certain environnement. Or, chacune de ces trois composantes dispose de caractéristiques bien spécifiques qu'il peut être intéressant d'exploiter en synthèse d'images. C'est ce que nous nous proposons de faire à travers une métrique perceptuelle entre images développée pour correspondre à nos besoins. Cette métrique permet de comparer deux images en utilisant un modèle de vision qui simule le traitement effectué par le système visuel humain. Elle sera ensuite intégrée dans un algorithme de rendu progressif, afin de remplacer les critères empiriques de ce dernier par des critères perceptuels. Les temps de calculs obtenus sont pratiquement deux fois inférieurs à ceux d'un calcul complet.
Dans le domaine de la synthèse d'images et de la réalité virtuelle, on appelle rendu l'étape qui consiste à calculer la couleur à afficher en chaque pixel de l'écran. Dans cet exposé, je présenterai deux problèmes de rendu : le rendu photo-réaliste et le rendu non photo-réaliste. Le premier problème correspond au calcul d'images indiscernables de la photographie de la même scène, donc à la simulation du comportement de la lumière. Après avoir présenté l'équation de rendu qui modélise le problème, j'exposerai quelques méthodes qui permettent de résoudre cette équation, notamment celle des vecteurs lumineux qui a été développée à l'Ecole Nationale Supérieure des Mines de Saint Etienne et à l'Université Lyon 1. Le second problème correspond à la recherche de simulation d'effets de style (peinture à l'huile, aquarelle, gravure, ...). Quelques exemples de travaux français sur ce thème seront présentés.
Généralement, les surfaces implicites à squelette utilisent des primitives simples telles que des points et des segments. En effet, l'étape de visualisation a souvent été un frein à une utilisation plus vaste de ce modèle. Des recherches récentes ont démontré la puissance créatrice des courbes et surfaces de subdivision en modélisation. Ce travail cherche à étendre le champ de modélisation des surfaces implicites à squelette par l'introduction de primitives à squelette plus complexe fondés sur des courbes, des surfaces et des volumes, puis en combinant ces squelettes à l'aide d'opérateurs de mélange localisé offrant un plus grand contrôle. Nous montrons que les primitives complexes qui sont très attractives pour la modélisation de par la grande diversité de formes qu'elles permettent, peuvent être visualisées efficacement afin de permettre une édition interactive. Nous présentons différentes méthodes de manipulation de ces primitives complexes. Nous avons adapté des techniques bien connues d'optimisation d'arbres et des algorithmes de ré-équilibrage afin d'accélérer les calculs. Nous proposons également des méthodes de pré-traitements communes à des classes de primitives et qui sont utiles à la fois pour une visualisation par lancer de rayons et par maillage. Enfin, nous décrivons notre implémentation des niveaux de détail tant au sein des primitives que des opérateurs qui permettent dès lors des modèles multi-résolutions et multi-représentations. Nous présentons finalement de nombreux exemples qui démontrent que notre système de modélisation par surfaces implicites peut être utilisé pour créer et animer des formes complexes de manière efficace.
Les protocoles cryptographiques sont des spécifications de suites de messages entre agents, utilisant des moyens de chiffrement (entre autres), et cherchant à assurer des besoins en confidentialité, authentification, ou d'autres propriétés. Je présenterai brièvement quelques façons d'attaquer le problème de leur vérification formelle. Une est fondée sur le modèle dit de Dolev-Yao, et peut se résoudre à l'aide d'automates d'arbres étendus ; lorsqu'on cherche à inclure dans le modèle la primitive de Diffie-Hellman, on tombe naturellement sur des extensions nouvelles de réseaux de Petri. Une autre façon d'attaquer le problème vient de la théorie des langages de programmation, et consiste à trouver des relations logiques pour des langages d'ordre supérieur avec création de noms et types de données cryptographiques.
Nous travaillons à l'implantation et la caractérisation des opérations numériques en machine dans le cadre du groupe de travail commun aux GDR ARP et ALP. Dans l'introduction de mon exposé, je présenterai deux exemples parmi tant d'autres de motivation de notre travail ainsi que les équipes participantes. Nous verrons ainsi que les applications sont très variées bien qu'elles reposent sur une culture commune. On distinguera les réalisations matérielles dont certaines sur FPGA des réalisations logicielles avec des nombres entiers ou à virgule flottante. Nous parlerons de la taille de l'implantation, de la consommation électrique, de la correction du résultat ou du contrôle des inévitables erreurs numériques. La division et l'approximation des fonctions élémentaires ou spéciales sont aujourd'hui des questions porteuses du domaine. Nous finirons ce tour d'horizon en remettant en cause l'architecture usuelle des calculs et les notations utilisées. Le dernier tiers de l'exposé sera consacré à notre effort nouveau de caractérisation précise de petits programmes numériques travaillant en précision limitée. Des outils mathématiques peuvent caractériser, automatiquement ou non, un comportement plus ou moins « typique » ou « pessimiste » de gros programmes numériques. On voudrait toutefois être capables de suivre les différentes erreurs d'arrondi introduites dans un code pour en déduire des propriétés exploitables et toujours vérifiées. Cela semble encore impossible pour les gros programme. Par contre, cet effort peut porter ses fruits s'il est appliqué à de petits programmes judicieusement choisis.Les transparents sont disponibles.
L'objet de la tomographie discrète est la reconstruction d'un objet discret à partir de ses projections. Nous allons présenter quelques problèmes de base de cette discipline comme la reconstruction de matrices booléennes, de tableaux colorés ou de pavages par des dominos. Nous formulerons aussi ces problèmes en termes de graphes, d'ordonnancements et présenterons quelques applications concernant la construction de planning de personnel. La reconstruction d'un objet n'est pas toujours possible, dans ce cas nous proposerons des problèmes d'optimisation permettant d'obtenir des reconstructions approchées. Nous illustrerons par l'intermédiaire de ces problèmes, certaines problématiques de l'optimisation combinatoire ainsi que les liens existants avec certaines disciplines voisines comme la Combinatoire, La Théorie de la Complexité.
C'est dans le but de résoudre des problèmes d'ordonnancement avec des fonctions de coût irrégulières que nous nous intéressons au problème d'affectation continue. Ce problème consiste à partitioner une région à d dimensions en sous-régions de volumes fixés, de manière à ce que le coût total soit minimisé. Le problème dual revient à maximiser sans contraintes une fonction concave mais non différentiable. La variante préemptive du problème d'ordonnancement avec critères irrégulier correspond au problème d'affectation en dimension 1 et une borne inférieure peut en être déduite pour la variante non préemptive. Cette borne est testée expérimentalement dans un algorithme par séparation et évaluation. Un preprint est disponible.
Le sac-à-dos multidimensionnel en 0-1 est NP-difficile et formalise de nombreux problèmes pratiques tels que le placement de capitaux, le chargement de cargaison, la gestion de stock et l'allocation de ressources partagées dans les systèmes distribués.
L'approche proposée ici exploite essentiellement des résultats obtenus par la programmation linéaire pour réduire l'espace de recherche S={0,1}n exploré par une méthode de voisinage.
Le simplex est utilisé dans un premier temps, pour définir des hyperplans à nombre d'objets
constants, puis pour choisir les variables de séparation dans une recherche arborescente de profondeur limitée, et enfin pour calculer les optima fractionnaires autour desquels une
intensification de la recherche est menée.
Cette phase d’échantillonnage d'une zone prometteuse de l'hypercube S est réalisée par un algorithme tabou. Sa caractéristique principale est une mémorisation complète des configurations visitées par la mis en œuvre de la méthode d'élimination inverse. La recherche ne peut donc pas cycler et garantit de produire autant de points distincts dans S que de mouvements effectués.
L'algorithme ainsi obtenu, hybride la programmation linéaire, l'énumération partielle et la recherche tabou. Il obtient les meilleurs résultats connus sur de nombreux benchmarks jugés difficiles. Nous observons par ailleurs que les sous-problèmes traités par la recherche
tabou partagent des caractéristiques communes et sont pratiquement intraitables par une approche exacte.
L'algorithmique dite "on-line" est apparue pour modéliser des situations où l'instance d'un problème n'est pas entièrement connue quand commence la résolution effective, par exemple si l'on se place dans l'optique d'une résolution en temps réel. L'instance du problème est alors "révélée" étape par étape, le but étant de construire, au cours de ce processus où l'on découvre l'instance, une solution réalisable la meilleure possible. Beaucoup de problèmes d'optimisation combinatoire ont ainsi été étudiés dans ce nouveau cadre, en particulier des problèmes sur les graphes. Nous nous sommes intéressés à différentes versions on-line (correspondant à différentes règles régissant la manière dont le graphe est révélé et celle dont l'algorithme peut construire sa solution) d'un problème bien connu : la recherche d'un stable de cardinalité maximale dans un graphe. L'étude de ces problèmes est menée dans l'optique d'examiner leur approximabilité (résultats positifs et négatifs), le cadre on-line constituant un prolongement naturel de la théorie de l'approximation pour les problèmes classiques.
Les algorithmes probabilistes auto-stabilisants sont ceux qui, partant d'une configuration initiale quelconque, atteignent un ensemble L de configurations, dites « légitimes », avec probabilité 1. La preuve classique de convergence vers L, se fait en exhibant une mesure sur les configurations qui décroît à chaque étape d'exécution, tant que L n'est pas atteint. Cette mesure, spécifique de chaque algorithme, est généralement difficile à trouver. Nous proposons ici une nouvelle méthode de preuve, inspirée de la notion de champ de Gibbs utilisée en Physique Statistique : à chaque trace d'exécution de l'algorithme nous associons une énergie ; pour assurer la convergence de l'algorithme, il suffit alors de montrer que les traces atteignant L ont une énergie « beaucoup » plus faible que les autres. Nous illustrons la méthode en donnant une preuve originale de l'auto-stabilisation de l'algorithme d'Herman.
Un système linéaire fini est un ensemble fini de fonctions linéaires dont les domaines de définition sont décrits par des formules de Presburger, et dont les matrices carrées associées engendrent un monoïde multiplicatif fini. On prouve que pour ces systèmes, l'accélération d'une séquence de fonctions peut être effectivement décrite dans la logique de Presburger. On montre alors que le nombre de bonnes séquences de fonctions de longueur n est polynomial en n alors que le nombre total de séquences de longueur n est exponentiel en n. Ces résultats théoriques sont implémentés dans l'outil FAST (Fast Acceleration of Symbolic Transition systems). FAST calcule en quelques secondes une représentation canonique de l'ensemble d'accessibilité de 8 protocoles broadcasts bien connus. Un rapport de recherche est disponible.
La vérification des systèmes continus et hybrides attire l'attention des chercheurs depuis une douzaine d'années. Vers 1995 la décidabilité de ce genre de problèmes semblait être bien explorée: en gros tout est indécidable sauf plusieurs cas particuliers. Après un bref survol de ces résultats on discutera le progrès récent dans le domaine et on essayera de convaincre l'audience de la richesse et de la complexité du domaine en abordant les questions suivantes: bruit et décidabilité; entre décidable et indécidable; méthode d'accélération pour vérifier les systèmes continus. A la fin de l'exposé on fera la comparaison de l'approche décrite avec celles de l'analyse constructive et de la complexité algébrique.
Nous présenterons une méthode de modélisation et de validation de programmes distribués sur des réseaux d'interconnexion symétriques. Nous appliquerons cette méthode pour la validation d'un algorithme sur hypercubes permettant le calcul parallèle du contour d'une image. Les preuves sont paramétrés sur l'ordre du réseau (nombre de processeurs). Le modèle formel choisi pour la représentation des réseaux dans l'environnement de démonstration automatique est basé sur le concept de graphe de Cayley. Notre méthode prend en compte les opérations de communication collectives (diffusion, distribution, réduction, ...) utilisées par les applications distribuées. La modélisation et la méthode de preuve développées permettent entre autres de s'abstraire du problème des communications point-a-point et de raisonner au niveau du processeur. De plus, elle permet d'obtenir automatiquement les invariants nécessaires aux preuvesTravail en collaboration avec Laurence Pierre publié dans "Mechanical Verification of Hypercube Algorithms" in FMPPTA 2002 , 7th International Workshop on Formal Methods for Parallel Programming: Theory and Applications. April 2002, Fort Lauderdale, Florida. IEEE Computer Society Press.
Un génome G1 se modélise sous la forme G1={S1,S2 ... Sm}, où chaque Si est un chromosome, c'est-à-dire un ensemble de gènes choisis dans {g1,g2 ... gN}. La distance synténique entre deux génomes G1 et G2 est définie comme le nombre minimum d'opérations permettant de passer de l'un à l'autre, où les 3 opérations autorisées, issues des observations des biologistes, sont les suivantes :
- fusion : deux chromosomes fusionnent pour n'en former qu'un
- fission : un chromosome se partitionne en deux chromosomes
- translocation : deux chromosomes échangent des sous-ensembles de leurs gènes. Il a été démontré que la plus grande distance possible existant entre deux génomes à (respectivement) m et n chromosomes est égale à m+n-4. Dans cet exposé, nous poursuivons cette étude en répondant à une question ouverte de Kleinberg et Liben-Nowell sur la caractérisation des instances représentant des génomes à distance synténique maximale (c'est-à-dire, m+n-4) l'un de l'autre. Ce résultat repose entre autres sur une propriété démontrant l'équivalence entre la translocation et un problème étudié depuis longtemps dans le domaine des réseaux d'interconnexion : le « gossiping ». (travail commun avec Cédric Chauve, LaCIM, Montréal)
Nous considérons deux applications du domaine de la bioinformatique : la première concerne le problème de reconnaissance de repliement de protéines, la deuxième - le problème de fragmentation de génomes bactériens. Dans les deux cas nous proposons plusieurs formulations MIP (Mixed-Integer Programming) et nous les résolvons en utilisant le logiciel CPLEX d'ILOG. Les résultats sont comparés avec d'autres approches connues de la littérature. Dans le cas du problème de reconnaissance de repliement de protéines et dans le cadre du dernier modèle MIP, l'optimum de toutes les instances que nous avons résolues, et qui sont basées sur des données « réelles » (utilisées par les biologistes), est atteint dans un sommet (0,1) du polytope sous-jacent. Les résultats numériques sont meilleurs que les résultats obtenus par un algorithme branch_and_bound dédié au problème.