Jeudi 2 Avril
Heure: |
12:15 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Extraction non supervisée de classes évolutives à partir de données temporelles |
Description: |
Allou Samé La classification de données évoluant au cours du temps constitue une problématique centrale dans de nombreuses applications. Dans ce cadre, les paramètres des classes doivent pouvoir sadapter à lévolution potentiellement non stationnaire des données. Cet exposé montrera comment les mélanges de lois peuvent être exploités, conjointement avec les modèles à espace détat (filtre de Kalman), pour atteindre cet objectif. Partant de ce formalisme, un algorithme EM variationnel et sa version online seront détaillés. Ceux-ci seront illustrés sur des données simulées et des données réelles dans le cadre dun problème de diagnostic dans le secteur ferroviaire. |
Mardi 7 Avril
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Structure algébrique des opérateurs de Fliess. |
Description: |
Loïc Foissy |
Heure: |
15:00 - 18:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Présoutenance de thèse : A left/right dynamic on permutations |
Description: |
Quentin de Mourgues Soit s une permutation dans Sigma_n.Soit i(s)=s(1), j(s)=s^{-1}(1),Soit C_k le cycle 1>2>...>(k-1)>1 (k,k+1,..,n points fixes).On definit L et R comme suit:L(s) = C_{j(s)}.s etR(s) = s.C_{i(s)}^{-1}Il est facile de voir que L et R sont inversibles, la dynamique L/R partitionne donc Sigma_n en classes d'équivalence qui sont des graphes orientés uniformes (une arête entrant/sortant par "couleur" L et R) fortement connexes.Dans cet exposé, on étudiera ces classes : leur nombre, leur taille, leur structure, etc. |
Heure: |
16:00 - 19:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Présoutenance de thèse : Tilings |
Description: |
Alexandra Ugolnikova |
Jeudi 9 Avril
Heure: |
14:30 - 15:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Enhanced Distributed Behavioral Cartography of Parametric Timed Automata |
Description: |
Hoang Gia Nguyen Parametric timed automata (PTA) allow the specification and verification of timed systems incompletely specified, or subject to future changes. The behavioral cartography splits the parameter space of PTA in tiles in which the discrete behavior is uniform. Applications include the optimization of timing constants, and the measure of the system robustness w.r.t. the untimed language. Here, we present enhanced distributed master-worker algorithms to compute the cartography efficiently. Experimental results show that our new algorithms significantly outperform previous distribution techniques. |
Mardi 14 Avril
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Diamètre et hamiltonicité des associaèdres de graphe |
Jeudi 16 Avril
Heure: |
14:30 - 15:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
"Formalising Concurrent UML State Machines Using Coloured Petri Nets" |
Description: |
Mohamed Mahdi Benmoussa While UML state machines are widely used to specify dynamic systems behaviours, their semantics is described informally, which prevents the complex systems verification. In this paper, we propose a formalisation of concurrent UML state machines using coloured Petri nets. We consider in particular concurrent aspects (orthogonal regions, forks, joins, shared variables), the hierarchy induced by composite states and their associated activities, internal/external/local transitions, and entry/exit/do behaviours. |
Vendredi 17 Avril
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
gdt Homotopy Type Theory - séance 1 |
Description: |
Andrew Polonsky The first of a little series of talks on Homotopy Type Theory (i.e., higher-order algebraic treatment of the notion of equality in dependant type theory).
Logical relations are a technique for proving meta-theoretic properties of type systems. In recent years, they have received a lot of attention as it became clear that logical relations give the most natural definition of extensional equality in type theory. A major open problem is to define a type system which contains extensional equality as an internal type constructor. For this, it is necessary to reflect the external logical relation back into the syntax of the type language. In this talk I will describe how to do this. |
Mardi 21 Avril
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
La tour de Hanoï, revue par Dudeney |
Description: |
Thierry Bousch Dans la version classique de "la Tour de Hanoï", c'est-à-direavec trois aiguilles, on sait bien qu'on peut transférer N disquesd'une aiguille vers une autre en 2^N-1 mouvements, et que ce nombreest minimal. Ajoutons une quatrième aiguille: quel est alors le nombreminimum de mouvements nécessaires pour transférer N disques d'uneaiguille vers une autre? Etrangement, ce problème posé il y a plusd'un siècle par le puzzliste anglais Henry Ernest Dudeney n'a étérésolu que tout récemment. Et pour d'autres variantes de la Tourde Hanoï, avec davantage d'aiguilles ou des restrictions sur lesmouvements, le problème est largement ouvert.voir aussi l'article sur le site du CNRS |
Mardi 28 Avril
Heure: |
12:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Exact Algorithms for Nonconvex Quadratic Integer Optimization |
Description: |
Christoph Buchheim The talk addresses the problem of minimizing a quadratic objective function over integer variables. Even in the most simple case of binary or box-constrained integer variables, such problems are very hard to solve in theory and in practice. In fact, the problem remains NP-hard both in the case of a convex objective function over binary variables (then being equivalent to max-cut) and in the case of a non-convex objective function over the unit cube (the so-called BoxQP).
After shortly reviewing some classical approaches for quadratic discrete optimization, we present two recent methods that are specifically designed for the nonconvex case, aiming at relaxations that jointly address the nonconvexity of the objective function and the nonconvexity of the discrete variable domains. While the first approach results in a semidefinite relaxation of the problem, the second approach uses ellipsoidal relaxations; both approaches can be embedded into branch-and-bound schemes. We present experimental results for the resulting algorithms, showing that the SDP-based approach yields very strong dual bounds that however take more time to be computed, while the second approach based on ellipsoidal relaxations is able to enumerate a large number of nodes in a short time due to a sophisticated preprocessing phase. The resulting total running times are comparable; both approaches however significantly outperform standard software such as Couenne or BARON. |
Mardi 5 Mai
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Comptage et énumération de surfaces plates, formes quasimodulaires |
Description: |
Samuel Lelièvre |
Jeudi 7 Mai
Heure: |
15:00 - 18:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Présoutenance de thèse : A left/right dynamic on permutations |
Description: |
Quentin de Mourgues Soit s une permutation dans Sigma_n.Soit i(s)=s(1), j(s)=s^{-1}(1),Soit C_k le cycle 1>2>...>(k-1)>1 (k,k+1,..,n points fixes).On definit L et R comme suit:L(s) = C_{j(s)}.s etR(s) = s.C_{i(s)}^{-1}Il est facile de voir que L et R sont inversibles, la dynamique L/R partitionne donc Sigma_n en classes d'équivalence qui sont des graphes orientés uniformes (une arête entrant/sortant par "couleur" L et R) fortement connexes.Dans cet exposé, on étudiera ces classes : leur nombre, leur taille, leur structure, etc. |
Heure: |
16:00 - 19:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Présoutenance de thèse : Tilings |
Description: |
Alexandra Ugolnikova |
Lundi 11 Mai
Heure: |
14:00 - 15:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Structured Prediction, Optimization and Deep Syntax |
Description: |
Caio Filippo Corro A sequence of words is not a sufficient representation for efficient processing of natural languages. In order to extract information from sentences, we need to decode their underlying abstract structure(s). Unfortunately, grammar formalisms that are able to properly capture complicated phenomena encountered in natural languages (wh-movements, cross-serial dependencies,...) have a repelling complexity. The work in this thesis will focus on developing efficient parsing algorithms for various formalisms (TAG, LCFRS, RCG) using optimization methods (Lagrangian relaxation, dual decomposition). |
Mardi 12 Mai
Heure: |
11:00 - 14:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Various aspects of automaton synchronization |
Description: |
Mikhael Berlinkov |
Heure: |
12:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
EXACT APPROACHES TO THE NETWORK DESIGN PROBLEM WITH RELAYS |
Description: |
Ivana Ljubic This work considers the Network Design Problem with Relays (NDPR). The NDPR arises in the context of network design when given node-pairs need to communicate with each other, but, due to signal deterioration, communication paths have to respect given distance limits. To cover longer distances, equipment for signal regeneration (i.e., relays) may be required. To enable required communications, one has to upgrade the network: by installing new links, by installing relays on the existing network, or by a combination of both. Besides applications in network design, the NDPR arises in the context of e-mobility where relays model charging stations for electric cars and edge costs correspond to road tolls.
In contrast to previous work on the NDPR, which was mainly focused on heuristic approaches, we propose new exact approaches based on different mixed integer linear programming formulations for the problem. We develop Branch-and-Price and Branch-Price-and-Cut algorithms that build upon models with an exponential number of constraints and variables. In a computational study, we analyze the performance of these approaches for instances with different characteristics.
This is a joint work with M. Leitner, M. Riedler and M. Ruthmair |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Énumération d'automates minimaux et fonctions de parking |
Description: |
Jean-Baptiste Priez |
Mardi 19 Mai
Heure: |
12:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Approximating the energy storage problem and other continuous dynamic programs |
Description: |
Giacomo Nannicini We study the problem of optimally managing a source of renewable energy connected to the power grid, a battery, and potentially a household or some other form of energy sink. This problem can be naturally cast as a dynamic program. We propose a model for this problem that subsumes other models in the literature, and we analyze its complexity, showing that in the deterministic setting the problem is solvable in polynomial time, but it becomes #P-hard in the stochastic setting. A variant of the problem that is commonly encountered in practice (i.e. the one where selling energy to the power grid is not allowed) admits a Fully Polynomial Time Approximation Scheme (FPTAS) if the energy levels are discretized; but what about the more natural case where energy is considered a continuous variable? We show that in this case, the problem belongs to a class of convex continuous dynamic programs that admits neither a multiplicative nor an additive approximation. We then show that we can construct a novel type of approximation scheme, where additive and multiplicative approximation are required at the same time but both can be arbitrarily small. We discuss a preliminary computational evaluation of this new type of approximation scheme for continuous convex dynamic programs, showing its potential. |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Explicit forms and combinatorial content of Levy stable distributions |
Description: |
Katarzyna Górska |
Jeudi 21 Mai
Heure: |
14:30 - 15:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Reachability Preservation Based Parameter Synthesis for Timed Automata |
Description: |
Étienne André The synthesis of timing parameters consists in deriving conditions on the timing constants of a concurrent system such that it meets its specification. Parametric timed automata are a powerful formalism for parameter synthesis, although most problems are undecidable. We first address here the following reachability preservation problem: given a reference parameter valuation and a (bad) control state, do there exist other parameter valuations that reach this control state iff the reference parameter valuation does? We show that this problem is undecidable, and introduce a procedure that outputs a possibly underapproximated answer. We then show that our procedure can efficiently replace the behavioral cartography to partition a bounded parameter subspace into good and bad subparts; furthermore, our procedure can even outperform the classical bad-state driven parameter synthesis semi-algorithm, especially when distributed on a cluster. |
Mardi 26 Mai
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Efficient Algebraic Diagonals and Walks |
Description: |
Louis Dumont The diagonal of a multivariate power series F is the univariate power series Diag F generated by the diagonal terms of F. Diagonals form an important class of power series; they occur frequently in number theory, theoretical physics and enumerative combinatorics. Westudy algorithmic questions related to diagonals in the case where F is the Taylor expansion of a bivariate rational function. It is classical that in this case Diag F is an algebraic function. We propose an algorithm that computes an annihilating polynomial forDiag F. Generically, it is its minimal polynomial and is obtained in time quasi-linear in its size. We show that this minimal polynomial has an exponential size with respect to the degree of the input rational function. Throughout the talk, we use a common problemof counting certain lattice walks to illustrate the capacities and limits of our tools. |
Mercredi 27 Mai
Heure: |
14:00 - 16:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Logics via algebras and substitutions |
Description: |
Antonino Salibra In this talk we present a translation of formulas and models of classical and non-classical logics into factor algebras. The correspondence: Propositional variables --- operator of decompositions Logical operations --- substitutions Formulas --- algebraic terms Models --- factor algebras, provides a uniform calculus of provability for all the logics which admit the translation. Many examples will be discussed: classical logic, intuitionistic logic, linear logic, many-valued logics. |
Mardi 2 Juin
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Explicit forms and combinatorial content of Levy stable distributions |
Description: |
Katarzyna Górska |
Vendredi 5 Juin
Heure: |
11:00 - 12:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Configuration Structures |
Description: |
Clément Aubert A standard contextual equivalence for process algebras is strong barbed congruence. Configuration structures are a denotational semantics for processes in which one can define equivalences that are more discriminating, i.e. that distinguish the denotation of terms equated by barbed congruence. Hereditary history preserving bisimulation (hhpb) is such a relation. We define a strong back and forth barbed congruence using a reversible process algebra and show that the relation induced by the back and forth congruence is equivalent to hhpb. Hence we give a characterization of hhpb as a contextual equivalence in a reversible process algebra.
Joint work with Ioana Cristescu. |
Mardi 9 Juin
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Calculabilité et pavages |
Description: |
Pascal Vanier |
Vendredi 12 Juin
Heure: |
11:00 - 12:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
On the dependencies of logical rules |
Description: |
Alexis Saurin Many correctness criteria have been proposed since linear logic was introduced and it is not clear how they relate to each other. We present proof-nets and their correctness criteria from the perspective of dependency, as introduced by Mogbil and Jacobé de Naurois.
More precisely, we introduce a new correctness criterion, called DepGraph, and show that together with Danos' contractibility criterion and Mogbil and Naurois criterion, they form the three faces of a notion of dependency which is crucial for correctness of proof-structures.
Finally, we extract the logical meaning of the dependency relation and show that it allows to recover and characterize some constraints on the ordering of inferences which are implicit in the proof-net.
Joint work with Marc Bagnol and Amina Doumane. |
Mardi 16 Juin
Heure: |
12:15 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Évaluation et sélection des collaborateurs en clustering collaboratif |
Description: |
Guénaël Cabanes L'objectif du clustering collaboratif est de révéler la structure commune de données qui sont réparties sur différents sites. Le concept fondamental du clustering collaboratif est d'avoir des algorithmes qui s'exécutent localement mais qui collaborent en échangeant de l'information sur les partitions locales des données obtenues par chaque algorithme. Ce type d'apprentissage collaboratif peut être appliqué à un grand nombre de tâches, y compris le clustering multi-vues, la segmentation de données distribuées, le regroupement et l'analyse multi-échelle et multi-expert, etc.... Cette étude introduit un nouveau cadre de collaboration qui permet à un large éventail d'algorithmes de collaborer ensemble. L'originalité de la méthode proposée est qu'elle rend possible la collaboration entre des algorithmes de différentes familles. Nous avons aussi analysé limpact de la diversité entre les collaborateurs et de la qualité des collaborateurs sur la qualité de la collaboration, afin de définir des pondérations à appliquer à chaque collaborateur. Nous avons testé l'efficacité de notre approche à partir dexpériences sur des jeux de données réels. |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Hopf algebras and towers of monoids |
Description: |
Aladin Virmaux |
Jeudi 18 Juin
Heure: |
14:30 - 15:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Model-checking for efficient malware detection |
Description: |
Tayssir Touili The number of malware is growing extraordinarily fast. Therefore, it is important to have efficient malware detectors. Malware writers try to obfuscate their code by different techniques. Many of these well-known obfuscation techniques rely on operations on the stack such as inserting dead code by adding useless push and pop instructions, or hiding calls to the operating system, etc. Thus, it is important for malware detectors to be able to deal with the program's stack. In this talk I will show a new model-checking approach for malware detection that takes into account the behavior of the stack. Our approach consists in : (1) Modeling the program using a Pushdown System (PDS). (2) Introducing new logics, called SCTPL and SLTPL, to represent the malicious behavior. SCTPL (resp. SLTPL) can be seen as an extension of the branching-time temporal logic CTL (resp. the linear-time temporal logic LTL) with variables, quantifiers, and predicates over the stack. (3) Reducing the malware detection problem to the model-checking problem of PDSs against SCTPL/SLTPL formulas. We show how our new logics can be used to precisely express malicious behaviors that could not be specified by existing specification formalisms. We then consider the model-checking problem of PDSs against SCTPL/SLTPL specifications. We provide efficient algorithms to solve these problems. We implemented our techniques in a tool, and we applied it to detect several viruses. Our results are encouraging. In particular, our tool was able to detect more than 800 viruses. Several of these viruses could not be detected by well-known anti-viruses such as Avira, Avast, Norton, Kaspersky and McAfee. |
Mardi 23 Juin
Heure: |
10:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Journée MathStic 'Marches dans le quart de plan' |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Uniform random generation of walks in the quarter-plane |
Description: |
Marni Mishna |
Heure: |
15:00 - 18:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Walks in the quarter plane with arbitrary big jumps |
Description: |
Kilian Raschel |
Mercredi 24 Juin
Heure: |
10:15 - 13:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Accueil de la Journée MathStic 'Combinatoire et probabilités' (! c'est un mercredi) |
Heure: |
10:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Journée MathStic 'Marches dans le quart de plan' (! c'est un mercredi) |
Heure: |
11:30 - 14:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Statistics of the real roots of real random polynomials |
Description: |
Grégory Schehr |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Uniform random generation of walks in the quarter-plane |
Description: |
Marni Mishna |
Heure: |
14:00 - 15:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Uniform random generation of walks in the quarter-plane |
Description: |
Marni Mishna |
Heure: |
15:00 - 18:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Walks in the quarter plane with arbitrary big jumps |
Description: |
Kilian Raschel |
Heure: |
17:00 - 20:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
pot de clôture |
Lundi 29 Juin
Heure: |
12:15 - 13:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
BE-PUM: A tool of Binary Emulation for Pushdown Model generation |
Description: |
Quan Thanh Tho In this talk, we present the tool BE-PUM (Binary Emulation for PUshdown Model generation) for binary analysis. As suggested by its name, BE-PUM generates pushdown model, which is considered as a control flow graph (CFG) combined with a memory execution model. BE-PUM also introduces a concolic approach in order to generate CFG in a more precise manner. As such, BE-PUM is able to handle various popular obfuscation techniques of malwares, such as indirect jump or self- modification code. In experiments, we are able to produce models for around 1700 samples of real malware. Compared to JakStab and IDA Pro, two state-of-the-art tools in this field, BE-PUM shows better tracing ability, sometimes with significant differences. |
Heure: |
14:00 - 15:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Annotation et exploration de textes de spécialité - fragments d'une expérience |
Description: |
François Lévy, Sylvie Szulman Nous avons (ré)écrit un outil de manipulation conjointe d'annotations et de textes annotés, Omtat (One More Textual Annotation Tool) qui permet de visualiser les annotations et d'en ajouter, Les annotations, inspirées de Brat (Brat rapid annotation tool) peuvent porter sur une zone discontinue et qualifier des annotations-arguments. Un moteur de requêtes permet d'extraire et d'exploiter des ensembles de documents, phrases et annotations. Les premiers tests portent sur des textes de biologies et sur des textes juridiques, pour lesquels nous avons créé quelques types d'annotations spécialisées. Nous en profiterons pour dire en quoi spécialiser les annotations en tenant compte du domaine nous parait utile et tenter de convaincre que les résultats peuvent être intéressants. |
|
|