Le séminaire du Laboratoire

Programmation pour 2018

OCT
25
00:00
OCT
11
13:30
Les opérateurs de composition sur l'espace des fonctions holomorphes sur le disque : propriétés spectrales
SEP
3
13:30
Mobility-assisted data transmission systems for offloading conventional communication networks.
The number and storage capacity of the handled devices we carry with us everywhere has significantly increased. In this presentation, we present three pieces of work where we exploit the opportunity of transferring for free the data stored on such devices as their owners move according to their daily commute. In a first work, we present a transmission system that takes advantage of the daily trips made by car to offload large volumes of data from the Internet. Our systems extends cost effectively the capacity of the Internet by having cars transporting data over long distances. In a second work, we present a stand-alone cloud storage system targeting mobile users in urban environments. This system relies on a collection of strategically located wireless data storage equipments acting as file repositories where mobile users can upload and share their files to save storage space on their devices. In a last work, we address the problem of virtualizing the resources of large-scale mobile networks. This work focuses on the migration of virtual machines triggered by the reallocations of virtual resources or changes in the physical topology.
AOU
30
11:00
Efficient parameter synthesis using optimised state exploration strategies
Parametric timed automata are a powerful formalism to reason about, model and verify real-time systems in which some constraints are unknown, or subject to uncertainty. Parameter synthesis using parametric timed automata is very sensitive to the state space explosion problem. To mitigate this problem, we propose new exploration orders, and compare them with existing strategies. Such exploration orders are designed for breadth-first search and depth-first search, that are well-suited to analyse reachability and liveness properties, respectively. Experimental results using IMITATOR show that our new strategies significantly outperform existing approaches.
AOU
29
13:00
Théorie des modèles III : de Turing à Scott
Alain Busser
L'exposé d'Alain Busser de ce mercredi 29 août est avancé de 30 mn. Il se déroulera donc de 13h à 14h.
AOU
23
14:30
Constrained DPOR: Avoiding redundancies in the exploration of concurrent programs
Verification and testing of concurrent programs is challenged by the combinatorial explosion that arises by considering all possible ways in which processes/threads can interleave. Partial Order Reduction (POR) techniques avoid redundancies in the exploration of concurrent programs based on the idea that two interleavings can be considered equivalent if one can be obtained from the other by swapping adjacent, independent execution steps. This talk will overview recent context-sensitive, constrained, dynamic POR techniques incorporated in the SYCO system, a SYstematic testing tool for COncurrent programs. We will also describe recent applications of SYCO to verify Software-Defined Networks.
AOU
23
13:30
Compositional Program Analysis using Max-SMT
Recent developments on SMT solvers for non-linear polynomial constraints have become crucial to make the template-based (or constraint-based) method for program analysis effective in practice. Moreover, using Max-SMT (its optimization version) is the key to extend this approach to develop an automated compositional program verification method based on generating conditional inductive invariants. We build a bottom-up program verification framework that propagates preconditions of small program parts as postconditions for preceding program parts and can recover from failures when some precondition is not proved. These techniques have successfully been implemented within the VeryMax tool which currently can check safety, reachability and termination properties of C code. In this talk we will provide an overview of the Max-SMT solving techniques and its application to compositional program analysis.
AOU
16
13:30
Segmentation des lignes et des colonnes d’une matrice pour l’analyse des vidéos dans le cadre des véhicules autonomes
Dans la recherche sur les véhicules autonomes, nous sommes souvent amenés à étudier la similarité entre des images de l’environnement prises à différents moments (Birem et al., 2014). Les données résumées issues de séquences vidéo réelles (Korrapati et al., 2013) se présentent sous forme de matrices dans lesquelles des lieux différenciés (e.g. ligne droite, intersection...) correspondent à des blocs relativement homogènes. Le but est de proposer une méthode automatique pour estimer les frontières de ces blocs. Cette étude se place dans un cadre temporel puisqu’il s’agit de couper la vidéo à différents instants pour que les images des séquences entre deux coupures soient homogènes. Pour répondre à cette question, il existe des algorithmes développés pour l’analyse des données Hi-C de séquençage du génome issues de la biologie (Dixon et al., 2012) dont la problématique est similaire. En particulier, Brault et al. (2017a) proposent une segmentation rapide en supposant que les observations sont constantes par bloc à l’aide d’une procédure basée sur le LASSO (Least Absolute Shrinkage and Selection Operator) et Brault et al. (2017b) étudient une segmentation fondée sur des statistiques de rang que nous proposons d’utiliser. Dans cet exposé, nous aborderons la problématique de la segmentation des lignes et des colonnes des matrices de dissimilarité entre les différentes images d’une vidéo obtenue dans le cadre de l'étude des véhicules autonomes. Nous introduirons les deux modèles utilisés dans le cadre des données Hi-C et comparons leurs avantages et inconvénients sur les données simulées et sur l’application aux données réelles.
JUL
3
13:30
de Beltrami à Godel II
Alain Busser
JUN
28
15:00
Caractérisation des graphes de Cayley
JUN
22
13:00
Du colis de Beltrami aux théorèmes de Tarski et Gödel
Alain Busser
JUN
14
14:30
Convergence d’approximations pour des lois de conservation hyperboliques stochastiques scalaires.
Dans cet exposé, je parlerai d’équations aux dérivées partielles stochastiques, plus précisément de lois de conservation avec terme source stochastique. Après quelques réflexions sur le terme stochastique, souvent appelé bruit blanc gaussien, qui modélise des incertitudes dans l’évolution temporelle des quantités conservées, je donnerai une formulation cinétique des équations étudiées.
Un résultat d’unicité de la solution cinétique sera donné, puis des hypothèses qui permettront d’avoir la convergence de suites de solutions approchées, ainsi que l’existence d’une solution cinétique.
Ces résultats sont issus d’un article co-écrit avec Julien Vovelle et publié dans la revue Archive for Rational Mechanics and Analysis.
JUN
7
09:00
Journée de la Recherche.
MAI
31
10:00
Réponse intermédiaire ascendante : Les Méta-Données.
7,55 milliards d’étoiles à proximité d’un trou noir… 75 % d’entres elles glissant chaque jour un peu plus vers cet astre mystérieux, le quart restant gravitant non loin de celui-ci mais néanmoins condamné à devenir la cible de demain… Portable à la main, l’homo numericus délaisse, bon gré mal gré, au Réseau des réseaux, une partie substantielle de lui-même. L’Internet, à la mémoire ineffable, approfondit au fil du temps sa connaissance de l’homme connecté.
Certes, cet apprentissage nécessite en amont une collecte en masse de données à caractère personnel qui, par le truchement de traitements combinés, donnent forme unique aux identités virtuelles. Désir inassouvi de connaissance toutefois devant ces représentations de soi si incomplètes et évolutives ! La parfaite maitrise juridique du phénomène n’en devient que plus ardue ...
Fondée sur un raisonnement inductif, la recherche d’un premier niveau d’abstraction qui permettrait, d’une part, d’atteindre le même niveau de connaissance des « users » que la collecte en masse de leurs données personnelles et, d’autre part, de poser un régime juridique au socle précis et stable pourrait s’avérer potentiellement fructueuse. La méta-donnée, ou donnée sur la donnée, mérite attention et réflexions.
MAI
24
14:00
Problème de Cauchy pour des équations différentielles stochastiques, introduction aux processus de Wiener cylindriques.
Dans cet exposé, je comparerai les hypothèses qui donnent existence et unicité d’une solution au problème de Cauchy pour une équation différentielle stochastique (EDS) et les hypothèses qui donnent existence et unicité d’une solution au problème de Cauchy d’une loi de conservation hyperbolique scalaire avec terme source stochastique. Je présenterai l’approximation de la solution donnée par le schéma d’Euler Maruyama, je la comparerai à l’approximation donnée par le schéma des Volumes Finis pour la loi de conservation stochastique et aux différentes approximations utilisées pour démontrer la convergence du schéma des Volumes Finis.
Enfin, je présenterai les processus de Wiener cylindriques en faisant le lien avec les hypothèses données par Einstein sur le mouvement de particules suspendues dans un liquide.
MAI
3
13:30
Mouvement Brownien, intégrale d'Itô, équations différentielles stochastiques, 2e partie.
Après avoir introduit dans l’exposé précédent le Mouvement Brownien réel, donné certaines de ses propriétés et défini l’intégrale d’Itô, je présenterai dans cet exposé l’espace naturel dans lequel vit le hasard, à savoir un espace probabilisé complet, muni d’une filtration complète, continue à droite. Le calcul stochastique y sera introduit à travers l’intégration par partie stochastique et le Lemme d’Itô qui généralise la dérivée des fonctions composées. Je donnerai un résultat d’existence et d’unicité d’une solution à une équation différentielle stochastique généralisant le théorème de Cauchy-Lipschitz en déterministe. J’introduirai une généralisation possible des équations différentielles stochastiques au cas où le Mouvement Brownien n’est plus à valeurs dans R mais dans un espace de Hilbert séparable.
AVR
26
15:00
Principe de Phragmén–Lindelöf et quelques applications.
Il est bien connu qu'une fonction holomorphe $f$ sur un ouvert connexe borné $X$ vérifie $\sup_{x\in X}|f(x)| =\sup_{y\in \partial X}|f(y)|$, où $\partial X$ désigne la frontière de $X$. Lorsque X est non borné, ceci n'est plus vrai mais cependant, à la condition que la fonction holomorphe $f$ vérifie un certain type de croissance (dépendant de la géométrie de $X$), le principe précédent sera vrai : ce sont les <> qui ont des applications dans un grand nombre de domaines des mathématiques. Après avoir exposé en quoi consistent les principes de Phragmen-Lindel\"of, nous en montrerons une application concernant des sommes binomiales.
AVR
26
13:30
Conception du MOOC « Apprendre à coder avec Python » : premier retour d’expérience.
soon
AVR
19
10:30
Théorème de Paris-Harrington III.
A non-standard model of PA in which PH is false
AVR
12
14:00
Mouvement Brownien, intégrale d'Itô, équations différentielles stochastiques.
Les équations d'évolution, équations différentielles ou équations aux dérivées partielles, d'abord déterministes, se sont affinées au cours du XXe siècle, pour prendre en compte leur caractère aléatoire.
Lorsque l’accroissement temporel aléatoire est continu et suit une loi normale alors le Mouvement Brownien est l’objet mathématique utilisé pour le modéliser.
Dans cet exposé, je définirai le Mouvement Brownien, donnerai quelques propriétés de ses trajectoires, j'expliquerai comment ses accroissements infinitésimaux sont pris en compte dans les équations d'évolution, comment on somme ses accroissements infinitésimaux grâce à l'intégrale d'Itô, je donnerai quelques outils pour résoudre ces équations différentielles stochastiques.
Enfin, je généraliserai le Mouvement Brownien et l’intégrale d’Itô pour des équations d’évolution perturbées par une infinité d’accroissements browniens indépendants.
AVR
5
13:30
Théorème de Paris-Harrington II.
Ultrafilters, non-standard models; models with indiscernibles
MAR
29
15:00
Théorème de Paris-Harrington I.
Ramsey's theorem (infinite and finite forms); large sets of integers; formulation of PH and its derivation from the infinite form
MAR
29
13:30
Problème de Cauchy de lois de conservation hyperboliques scalaires - Présentation générale I.
Les lois de conservation sont des équations aux dérivées partielles issues de la physique. Les définitions de solution ont évolué au cours du XXe siècle pour aboutir à une définition de solution faible entropique due au mathématicien russe Kruzkov. Je présenterai ces différentes définitions, le théorème d'existence et d'unicité au problème de Cauchy de Kruzkov, les idées de la démonstration pour l'unicité de la solution faible entropique. Je présenterai une approximation numérique de la solution faible entropique par le schéma des Volumes finis, les idées de la démonstration de cette approximation vers la solution faible entropique. Je présenterai pour finir une formulation cinétique des lois de conservation où les mathématiciens Lions, Perthame et Tadmor introduisent une variable supplémentaire dite cinétique et une mesure de l'entropie mathématique.
FEV
22
13:30
Weather 3D au Laboratoire de l'Atmosphère et des Cyclones : une chaîne de production d'objets météorologiques en 3 dimensions pour une visualisation sur navigateur WebGL.
La quantité d’informations scientifiques que doit analyser quotidiennement le chercheur dans le domaine de l'atmosphère augmente de manière exponentielle.
Il doit traiter des fichiers de données de plus en plus importants en volume et en nombre. L'origine des data est également plus diverse allant de fichiers issus de modèles numériques aux observations 3D. Il devient clair que les outils traditionnels de représentation et d’analyse en 2D sont de plus en plus lourds à manipuler et qu’ils ne conviennent vraiment que lorsque le chercheur ou l’observateur a déjà une idée précise de la situation et des éléments à analyser. La visualisation 3D des données permet d'appréhender une situation plus rapidement et de construire une analyse plus affutée par l'optimisation du positionnement des coupes 2D, la représentation de l'évolution temporelle d'une situation en 3D sous différents angles de vue, etc.
Cependant, les outils de visualisation classiques en 3D présentent une courbe d’apprentissage souvent trop ardue. Ils demandent au chercheur un véritable investissement en temps pour maîtriser la manipulation de l’outil, des postes de travail performants et correctement configurés, mais aussi un travail informatique de conversion des données afin qu’elles soient assimilables par ces outils.
C’est dans ce contexte qu'intervient Weather3D : un outil peu gourmand en matériel puisqu’il ne nécessite qu’un navigateur, des données déjà formatées qui évitent aux chercheurs de perdre du temps en préparation informatique et une aide importante à l’analyse des situations étudiées.
FEV
15
14:30
A fixed point theorem for commuting families of relational homomorphisms with applications to metric spaces, oriented graphs and ordered sets.
We extend to binary relational systems the notion of compact and normal structure, introduced by J.P.Penot for metric spaces, and we prove that for the involutive and reflexive ones, every commuting family of relational homomorphisms has a common fixed point. The proof is based upon the clever argument that J.B.Baillon discovered in order to show that a similar conclusion holds for bounded hyperconvex metric spaces and then refined by Amine Khamsi. Since the non-expansive mappings are relational homomorphisms, our result includes those of T.C.Lim and J.B.Baillon. Also it extends the Tarski fixed point theorem to graphs which are retracts of reflexive oriented zigzags of bounded length.