Programme: 2011-2012

Yassamine Seladji (04/07/2012)

• Titre:
  Numerical Abstract Domain using Support Functions
• Résumé:
  
  Abstract interpretation based static analysis of numerical programs aims at computing invariants of the values that variables can take during any execution of the program. Most numerical domains can efficiently represent convex sets using a polyhedral representation. Another popular representation of convex sets is the use of support functions. In particular, support functions have been successfully used in the field of hybrid systems analysis to represent sets of values. In my talk, I will show you that it is possible to use support functions to define a new abstract domain that is simpler than the polyhedra domain and allows for efficient computation of linear operations.

Jean-Louis Boulanger (25/06/2012)

• Titre:
  Retours d'expérience concernant l'utilisation des méthodes formelles dans l'industrie
• Résumé:
  
  Depuis le premier système à base de logiciel (le SACEM), le développement du domaine ferroviaire a été accompagné du développement des méthodes formelles (méthode B, SCADE,...). Mais les autres domaines (Nucléaire, aéronautique, spatial et automobile) ont suivit le mouvement. Il est à noter que de manière plus large, nous sommes passé de l'utilisation discrète des méthode formelles à une mise en oeuvre plus intensive des techniques formelles (interprétation abstraite, preuve, model-checking, simulation, etc.). Dans le cadre de cet exposé, nous ferons le point de la situation et nous présenterons les nouvelles orientations (aspect système, formalisation des cahier des charges, aspect modèle, etc.)

Xavier Olive (11/04/2011)

• Titre:
  Programmation par contraintes: distribution, symétrie
• Résumé:
  
  La programmation par contraintes distribuée est un paradigme de définition de problèmes distribués. Un ensemble d'agents se partagent des variables définies sur un domaine, lesquelles sont reliées par différentes contraintes: certaines sont locales; d'autres sont globales et nécessitent une coordination entre agents pour parvenir à une satisfaction ou optimisation des contraintes. Cette distribution de la définition des données présente un intérêt certain quant au respect de la confidentialité: les agents sont prêts à coopérer pour résoudre un problème, mais pas forcément à partager toute l'information en leur possession.
  Par ailleurs, la recherche de symétries est un moyen connu d'optimiser le temps de résolution d'un problème de programmation par contraintes distribué. Je présenterai alors quelques méthodes de détection et d'exploitation des symétries dans des problèmes distribués de programmation par contraintes.

Bogdan Stanciulescu (18/03/2012)

• Titre:
  Perception et robotique en ITS : vers la Route Automatisée
• Résumé:
  
  Présentation des travaux de recherches de l'école des Mines paris dans le domaine de la perception et la robotique.

Cécile Braunstein (06/03/2012)

• Titre:
  Classification et quantification de la robustesse de circuits aux fautes transitoires par model-checking symbolique
• Résumé:
  
  Robustness analysis of RTL-sequential circuits impacted by transient faults is an important concern for designers. While simulation or emulation based techniques are widely used, they do not give guarantees on the robustness level of the system and are often limited to single fault models. Moreover, several robustness criterions may be adopted depending on the application being executed and the synchronization scheme between the circuit and its environment. The use of formal methods ensures robustness level and helps in locating weak portions of a circuit to be hardened, even in case of multiple fault models. We present a framework to analyze the robustness of a RTL circuit, considering several models of faults and reparation, and show how a wide class of robustness criteria can be mapped into our reparation model. We present an implementation of the robustness measures in the setting of BDD-based model checking and illustrate our measurements on classical benchmark circuits.

Antoine Manzanera (07/02/2012)

• Titre:
  1-to-1 Hough Transforms on Grey Level Images
• Résumé:
  
  The Hough transform is a classical and powerful tool for detecting parameterized shapes in images. Still today, it is mostly applied on binary images of contours or connected sets, which implies pre-processing of the images. Then, the transform on binary images is performed using either of the two classical dual approaches: (i) the many-to-1 projection, which picks n-tuples of points from the binary image and select the unique corresponding points in the n-dimensional parameter space, and (ii) the 1-to-many back-projection, which, for every point of the binary image, draws the corresponding (n-1)-manifold in the parameter space. Both methods have computational drawbacks, that get worse as the number of parameter increases. By locally estimating the spatial derivatives, one can perform a direct 1-to-1 projection from the image to the parameter space. Furthermore, this can be done directly on the grey level image, which makes these methods much faster. We will present the algorithms and show their results in the case of analytical shapes for order one (lines), and two (circles), and we will also present the generalized Hough transform based on quantized derivatives for detecting arbitrary (non-analytical) shapes.

Cédric Pasteur (31/01/2012)

• Titre:
  ReactiveML, un langage de haut-niveau pour la programmation de systèmes concurrents et réactifs
• Résumé:
  
  ReactiveML est une extension du langage OCaml avec des primitives synchrones, en particulier une notion d'instant logique global. Alors que les langages synchrones traditionnels comme Lustre ou Esterel sont utilisés pour la programmation de systèmes embarqués avec des contraintes de temps-réel, on s'intéresse ici à une programmation plus généraliste. ReactiveML est par exemple adapté pour la programmation de simulations discrète. Il a été utilisé avec succès pour l'outil GLONEMO de simulation de réseaux ad-hoc de capteurs. Nous présenterons dans un premier temps les bases du langage et du modèle de concurrence synchrone. Nous aborderons ensuite deux travaux récents: une extension du langage appelée domaines d'horloges et une implémentation parallèle et distribuée du langage.

Fabio Martìnez Carrillo (17/01/2012)

• Titre:
  Characterization and modelling of complex movements: A human action classification approach for surveillance applications
• Résumé:
  
  There exist many different domains in which the study of complex movement is a crucial issue. Each particular domain of application is characterized by its specificities, namely different sources or noise, different relationships and a different level of nonlinearity. In this presentation, we introduce a novel motion descriptor that enables human activity classification in video-surveillance applications. The method starts by computing a dense optical flow, providing instantaneous velocity information for every pixel. Then, the obtained flow is characterized for every frame by an orientation histogram weighted by the norm, the orientations being quantized to 8, 16 or 32 principal directions. Finally, a set of characteristics are calculated from the temporal series obtained from each histogram bin, forming a descriptor vector. With a typical descriptor dimension of 96, the method achieves a 96.2 % of accuracy in a classification task performed on a dataset of 150 short sequences, using a support vector machine (SVM) classifier.

Nicolas Ayache (13/12/2011)

• Titre:
  Certifying cost annotations in compilers
• Résumé:
  
  We discuss the problem of building a compiler which can lift in a provably correct way pieces of information on the execution cost of the object code to cost annotations on the source code. To this end, we need a clear and flexible picture of: (i) the meaning of cost annotations, (ii) the method to prove them sound and precise, and (iii) the way such proofs can be composed. We propose a so-called labelling approach to these three questions. As a first step, we examine its application to a toy compiler. This formal study suggests that the labelling approach has good compositionality and scalability properties. In order to provide further evidence for this claim, we report our successful experience in implementing and testing the labelling approach on top of a prototype compiler written in ocaml for (a large fragment of) the C language.

Sébastien Bardin (15/11/2011)

• Titre:
  Refinement-based CFG Reconstruction from Executable Files
• Résumé:
  
  Automatic analysis of programs from their executable files has many potential industrial applications, for example: automatic analysis of mobile code and malware, security testing, third-party certification or worst case execution time estimation. Control-Flow Graph reconstruction appears to be a cornerstone of safe binary-level analysis: if the recovery is unsafe, subsequent analyses will be unsafe too; if it is too rough, they will be blurred by too many unfeasible branches and instructions.
  We address the issue of recovering a both safe and precise approximation of the CFG of a program given as an executable file. The problem is tackled in an original way, with a refinement-based static analysis working over finite sets of constant values. Requirement propagation allows the analysis to automatically adjust the domain precision only where it is needed, resulting in precise CFG recovery at moderate cost. First experiments, including an industrial case study, show that the method outperforms standard analyses in terms of precision, efficiency or robustness.

Hajime Nagahara (04/11/2011)

• Titre:
  Extended Cameras
• Résumé:
  
  A camera technology is rapidly developed according to wide demand of a market. However, there still have been a lot of limitations, even if it is the latest digital camera since it is difficult to improve them by classical hardware solution. Recently, computational photography is getting popular to solve some of them by combining hardware and software solutions. In this talk, I will point out some limitations; field of view, sampling rate and depth of field and introduce my previous works; omnidirectional camera, hybrid sensor camera, focal sweep camera and programmable aperture camera for extending to these limitations. I will also show the applications in computer vision and graphics.

Natalia Lyubova (18/10/2011)

• Titre:
  Developmental learning for object perception
• Résumé:
  
  The goal of this work is to design a visual system for a humanoid robot, that supports efficient online object learning and recognition. We are detecting potential objects using saliency in the visual space, constructing mid-level features from several descriptors and building hierarchical multi-view representations of these salient regions. These salient regions are then categorized into categories such as robot parts, humans or manipulable objects. Our learning algorithm is only based on the statistics of feature occurrences without requiring any image databases for learning. All knowledge about possible objects are acquired gradually by interactive exploration of the visual space, by the analogy with child development as inspired by developmental robotics. Finally, such visual system is going to be implemented on the iCub robot as a part of MACSi project.

Alexandre Chapoutot (04/10/2011)

• Titre:
  An Introduction to Formal Methods of Software
• Résumé:
  
  The aim of this presentation is to introduce the main ideas behind the formal verification techniques for software. In particular, I will introduce an operational semantics of a small imperative language and an axiomatic semantics of this language. Finally, I will briefly present the static analysis by abstract interpretation.

Alexander Gepperth (20/09/2011)

• Titre:
  Developmental concept formation driven by predictability
• Résumé:
  
  I will present a novel approach to the open-ended development of internal concept representations in autonomous agents. For an autonomous agent with existing internal concepts, I propose that any new concept must be at least partially inferable ("predictable") from existing ones. To achieve this, I describe a neural learning paradigm which I term "PROPRE" (projection-prediction), which exploits the bi-directional interaction of clustering ("projection", here realized by a self-organizing map) and associative learning ("prediction", implemented by logistic regression). Key ingredient of the PROPRE paradigm is an easy-to-compute online measure of predictability derived from the "prediction" step, by which the clustering algorithm is encouraged to favor predictable clusters.
  I will describe several simulation experiments I have already conducted to show the value and feasibility of this approach. I will furthermore outline how to translate the simulation experiments into real-world robotic applications. These include

  1. a mobile robot acquiring a visual concept of "floor" by exploiting the "can drive over it" property,
  2. an intelligent car acquiring a "physical size" concept for visual traffic objects by exploiting their known identity,
  3. a mobile robot simultaneously developing Kinect- and camera-based visual object concepts by using correlations between the forming concept representations.