Schedule: 2013-2014

Laure Gonnord (ENS de Lyon/LIP) (13/06/2014)

• Title:
  Les seuls problèmes intéressants sont les problèmes indécidables application à la synthèse de preuve de terminaison de programmes.
• Abstract:
  

  Le problème de la preuve de terminaison de programme est bien connu pour être, dans le cas général, un problème indécidable. Ce constat étant fait, on peut quand même essayer de ne pas jeter complétement le bébé avec l'eau du bain. Le choix qui est fait ici est d'essayer de traiter le cas général par des algorithmes _conservatifs_ : si l'algorithme répond oui, alors le programme termine, dans le cas contraire, on ne peut conclure.

  Pour le cas qui nous intéresse, nous commençons par "prouver" que le programme termine en exhibant une fonction qui décroît à chaque transition et qui reste positive (fonction "de rang"). Pour ce faire, nous utilisons des algorithmes classiques en compilation et en analyse statique: compilation d'un programme vers un automate affine, calcul d'invariants polyédriques, et enfin nous adaptons un algorithme glouton de calcul d'un ordonnancement multidimensionnel pour calculer une fonction de ranking affine multidimensionnelle. J'exposerai ces techniques ainsi que l'algorithme final.

  Une fois la fonction de rang exhibée, nous sommes en mesure de calculer un effet de bord sympathique : une borne supérieure de la complexité pire cas du programme.

  J'exposerai ensuite nos résultats expérimentaux et les pistes que nous explorons actuellement pour améliorer le passage à l'échelle, ainsi que quelques applications à d'autres domaines que la "simple" preuve de terminaison, notamment l'utilisation dans le cadre des compilateurs "just-in-time".

François Pessaux (ENSTA paris/U2IS) (05/06/2014)

• Title:
  The FoCaLiZe language: mixing program and proofs
• Abstract:
  

  FoCaLiZe is a programming language allowing to state in a same framework algorithms (programming aspects), properties (logical aspects) that these algorithms must satisfy and proofs these latter hold. It provides high-level constructs to ease development structuring and reuse (modularity, inheritance, late-binding, parameterization) and a proof language allowing to write proofs in a hierarchical way, using a natural deduction style, which rely on the Zenon automated theorem prover to discharge goals ... and the burden of the user. The core programming language is a pure functional language while properties are stated a first-order logic formulae. A FoCaLiZe development is compiled in two target languages: one OCaml source code leading to an executable (or object file) and one Coq source code containing the complete model of the development (i.e. definitions, properties and proofs) that will be ultimately checked by Coq as assessment. A crucial care in this process is to avoid any error from the target languages being returned to the user: a program accepted by the FoCaLiZe compiler must be accepted by both OCaml and Coq. To increase confidence in "what is ran is what is proved" despite two target languages, the compiler has to use a code generation model identical and traceable for both of them.

  In this presentation we will introduce the motivations, design and features choices that impacted the language semantics. The presentation of the language features and the development style will also be addressed on the basis of examples, trying to illustrate advantages (and disavantages) of such a system compared to other existing formal proofs systems.

Pierre Roux (Université Paris-Sud/LRI) (22/05/2014)

• Title:
  Analyse statique de systèmes de contrôle commande : génération d'invariants non linéaires
• Abstract:
  

  Les systèmes critiques comme les commandes de vol peuvent entraîner des désastres en cas de dysfonctionnement. D'où l'intérêt porté à la fois par le monde industriel et académique aux méthodes de preuve formelle capable d'apporter, plus ou moins automatiquement, une preuve mathématique de correction. Parmi elles, cet exposé s'intéresse particulièrement à l'interprétation abstraite, une méthode efficace pour générer automatiquement des preuves de propriétés numériques qui sont essentielles dans notre contexte.

  Il est bien connu des automaticiens que les contrôleurs linéaires sont stables si et seulement si ils admettent un invariant quadratique (un ellipsoïde, d'un point de vue géométrique). Ils les appellent fonction de Lyapunnov quadratique et une première partie propose d'en calculer automatiquement pour des contrôleurs donnés comme paire de matrices. Ceci est réalisé en utilisant des outils de programmation semi-définie. Les aspects virgule flottante sont pris en compte, que ce soit dans les calculs effectués par le programme analysé ou dans les outils utilisés pour l'analyse.

  Toutefois, le véritable but est d'analyser des programmes implémentant des contrôleurs (et non des paires de matrices), incluant éventuellement des réinitialisation ou des saturations, donc non purement linéaires. L'itération sur les stratégies est une technique d'analyse statique récemment développée et bien adaptée à nos besoins. Toutefois, elle ne se marrie pas facilement avec les techniques classiques d'interprétation abstraite. La partie suivante propose une interface entre les deux mondes.

  Enfin, la dernière partie est un travail plus préliminaire sur l'usage de l'optimisation globale sur des polynômes basée sur les polynômes de Bernstein pour calculer des invariants polynomiaux sur des programmes polynomiaux.

Dominique Bereziat (UPMC/LIP6) (15/05/2014)

• Title:
  Assimilation variationnelle de données pour l'analyse d'images
• Abstract:
  

  L'assimilation de données désigne un ensemble de méthodes qui permettent de déterminer l'état d'un système à partir d'informations variées telles qu'un modèle et des observations pouvant être de nature diverse. Les filtres de Kalman sont, par exemple, des méthodes d'assimilation de données. Dans cet exposé, nous nous intéresserons à une famille d'approches variationnelles appelée 4D-Var. Le modèle est donné soit par le contexte expérimental (des lois physiques) soit par des heuristiques simples sur la dynamique d'évolution. Pour relier le vecteur d'état aux observations, il convient ensuite de définir un opérateur d'observation dont le rôle est de projeter l'espace des états dans celui des observations. Nous donnerons deux utilisations de 4D-Var: la première pour calculer une circulation de surface océanographique à partir d'images de température de surface, la seconde pour segmenter et suivre des nuages à partir d'acquisitions MétéoSAT.

Guy Le Besnerais (ONERA/DTIM) (14/04/2014)

• Title:
  Du capteur à la perception de l’environnement : travaux de recherche de l'axe Imove de l'ONERA/DTIM
• Abstract:
  

  Cette présentation fournit un panorama des travaux de recherche réalisés dans l'axe "Imove" (Image Mouvement Volume) du DTIM (Département de Traitement de l'Information et Modélisation) de l'ONERA. Cet axe est caractérisé par une approche globale et opportuniste de la vision par ordinateur, depuis les capacités optiques et électroniques des capteurs jusqu'à l'analyse du mouvement et la reconstruction du volume d'une scène dynamique et complexe. On présentera en particulier les activités liées à la co-conception de caméras RGB-d par mesure de défocalisation chromatique, le calcul temps réel du flux optique, la super-résolution, et les algorithmes de structure from motion. On évoquera aussi les modèles de performances proposés pour évaluer ces systèmes.

Dumitru Potop Butucaru (INRIA Rocquencourt) (13/03/2014)

• Title:
  The case for programmable on-chip interconnect
• Abstract:
  
  Various techniques for the mapping of application onto NoC-based MPSoCs already consider in great detail the allocation and scheduling of computations onto the CPU cores and the allocation of data onto the memory banks. On the other hand, the Network-on-Chip (NoC) interconnect provides less control to the programmer, especially concerning the arbitration. Therefore, the routing and arbitration of communications onto the NoC is usually controlled indirectly (through the mapping of computations and data) or through the tuning of QoS-like parameters. We will argue that better control of NoC arbitration is needed, especially for embedded applications. We will explain how more expressive NoC routers may help with application deployment, so as to harmonize the data transfers with local data computations. More precisely, the work presented here allows for some limited programmability inside those routers, so that they can establish effective static scheduling and routing as demanded by the application. Router programs are the result of a general compilation process which targets the NoC and the individual cores altogether. The result is an improvement of both speed and timing predictability.

Alain Darte (CNRS/ENS de Lyon) (27/02/2014)

• Title:
  Understanding and manipulating multi-dimensional loops: A short tour in the world of polyhedral techniques.
• Abstract:
  

  Loops are a fundamental control structure in programming languages. Being able to analyze, to transform, and to optimize loops is a key feature for compilers to handle repetitive schemes with a complexity proportional to the program size and not to the number of operations it describes. This is true for the generation of optimized software as well as for the generation of hardware, for both sequential and parallel execution. Irregular loops are in general handled by graph algorithms on (reducible or not) control-flow graphs. Regular multi-dimensional loops on the contrary are better captured by polyhedral representations on which polyhedral optimization techniques can be applied.

  Such polyhedral analysis/compilation techniques have been developed actively, year after year, since the end of the 80s. After a first phase of mostly theoretical results, the ``polyhedral community'' has put more efforts on making this theory practical, thanks to the development of polyhedral optimization tools and ``compilers''. The arrival of FPGAs, GPUs, multicores, and their increasing complexity have also strengthened the need for higher-level code analysis and optimizations, for which polyhedral techniques seem particularly useful.

  The goal of this talk is to give a (too) quick introduction to such polyhedral techniques, recalling seminal results and fundamental mathematical tools and mentioning some more recent advances from our group: program termination and WCET for loops, analysis of data races in the parallel language X10, automatic kernel offloading. I will describe more precisely this last problem, i.e., our current attempts to automatically design blocked, pipelined algorithms, with inter-block data reuse, for kernels to be offloaded to a distant platform (e.g., FPGA or GPU). It requires the full power of polyhedral techniques: parametric code analysis, parametric tiling, automatic array contraction for the local memory, polyhedral code generation.

Son Vu (ENSEA/ETIS) (20/02/2014)

• Title:
  Recent contributions to Texture Categorization and Facial Analysis
• Abstract:
  
  This talk presents recent contributions to texture categorization and facial analysis with respect to different stages. As preprocessing, two versions of retina filtering simulating the performance of human vision system are presented (one for illumination normalization on face images, and one for generating richer details on texture images). A series of descriptors encoding the relationship between different types of information (gradient, entropy) of local image structures is also presented. Those descriptors are discriminative and robust to exterior variations (viewpoint, illumination and image quality). Also, several improvements to the «congealing» model for joint image alignment are presented. All those methods producing the state-of-the-art performance are very fast and are therefore suitable for applications with real-time constraints.

Alexandre Chapoutot (ENSTA/U2IS) (16/01/2014)

• Title:
  Set-based simulation of hybrid systems: theory and applications
• Abstract:
  
  Hybrid systems are a widely used model to represent and reason about control-command systems. In an industrial context, these are often implemented in Simulink and their validity is checked by performing many numerical simulations in order to test their behavior with various possible inputs. In this presentation, we define a set-based simulation of hybrid systems with uncertain parameters, expressed in Simulink. Our method handles advanced features such as non-linear operations, zero-crossing events or discrete sampling. It is based on well-known efficient numerical algorithms that were adapted to handle set-based domains. In this presentation, we also consider the use of set-based simulation to the study of numerical properties of closed-loops systems with uncertainties such as the overshoot or settling time. Our technique consists in adding to the system a monitor that does not interact with the dynamics of the system but infers a desired property.

Stéphane HERBIN (ONERA/DTIM), Cédric LE BARZ (Thales + ONERA) (19/12/2013)

• Title:
  Interprétation de scène dynamique et aide à la navigation
• Abstract:
  
  Le département Traitement de l'Information et Modélisation de l'Onera mène des actions de recherche depuis plusieurs années sur la conception de traitements permettant de décrire le contenu de scènes dynamiques observées principalement par des capteurs aérospatiaux. L'exposé se déroulera en deux parties. La première présentera un panorama de quelques réalisations et problématiques allant de la détection jusqu'à la description sémantique hiérarchique d'objet. La deuxième se concentrera sur les travaux en cours d'aide à la navigation de mobiles autonomes par localisation visuelle.