Exposés longs de l'UE Séminaire 22-23

mardi 28 février Amphi du LaBRI :

  • 14h : Sylvain Rais Time-Varying Graphs and Dynamic Networks
    • Résumé : The past few years have seen intensive research efforts carried out in some apparently unrelated areas of dynamic systems -- delay-tolerant networks, opportunistic-mobility networks, social networks -- obtaining closely related insights. Indeed, the concepts discovered in these investigations can be viewed as parts of the same conceptual universe; and the formal models proposed so far to express some specific concepts are components of a larger formal description of this universe. The main contribution of this paper is to integrate the vast collection of concepts, formalisms, and results found in the literature into a unified framework, which we call TVG (for time-varying graphs). Using this framework, it is possible to express directly in the same formalism not only the concepts common to all those different areas, but also those specific to each. Based on this definitional work, employing both existing results and original observations, we present a hierarchical classification of TVGs; each class corresponds to a significant property examined in the distributed computing literature. We then examine how TVGs can be used to study the evolution of network properties, and propose different techniques, depending on whether the indicators for these properties are a-temporal (as in the majority of existing studies) or temporal. Finally, we briefly discuss the introduction of randomness in TVGs.
  • 14h45 : Pablo Leboulanger The power consumption of mobile and fixed network data services- The case of streaming video and downloading large files
    • Résumé : There are numerous claims in media about the electricity consumption of video streaming and data downloading over mobile and fixed networks. Reviewing these claims against recent data reveals many such claims to be inaccurate and out of range – often by orders of magnitude. Such claims are typically based on old energy per data figures for average use over time that cannot be applied to current very high data usages like video streaming and data downloading. Instead, as a more accurate and relevant method, this paper suggests that power models are used and suggests relevant parameter values for such models. Watching YouTube videos (a1 Mbps) on a smartphone including usage of networks and servers consume about 10 W on average. Streaming Netflix (4-5 Mbps) on fixed broadband add about 7 W, mainly from Netflix/partners data centers (servers), to the near constant 18 W power consumption of an average fixed broadband line including usage of higher order networks.
  • 15h30 : Martin Thioliere Mining Precise Test Oracle Modelled by FSM by Omer Nguena Timo
    • Résumé : Precise test oracles for reactive systems such as critical control systems and communication protocols can be modelled with deterministic finite state machines (FSMs). Among other roles, they serve in evaluating the correctness of systems under test. A great number of candidate precise oracles (shortly, candidates) can be produced at the system design phase due to uncertainties, e.g., when interpreting their requirements expressed in ambiguous natural languages. Selecting the proper candidate becomes challenging for an expert. We propose a test-driven approach to assist experts in this selection task. The approach uses a non deterministic FSM to represent the candidates, includes the partitioning of the candidates into subsets of candidates via Boolean encodings and requires the intervention of experts to select subsets. We perform an empirical evaluation of the applicability of the proposed approach.
  • 16h15 : Romain Delpy Error detection of asynchronous message passing programs in A. Bouajjani's article
    • Résumé :We address the problem of verifying message passing programs, defined as a set of processes communicating through unbounded FIFO buffers. We introduce a bounded analysis that explores a special type of computations, called k-synchronous. These computations can be viewed as (unbounded) sequences of interaction phases, each phase allowing at most k send actions (by different processes), followed by a sequence of receives corresponding to sends in the same phase. We give a procedure for deciding k-synchronizability of a program, i.e., whether every computation is equivalent (has the same happens-before relation) to one of its k-synchronous computations. We show that reachability over k-synchronous computations and checking k-synchronizability are both PSPACE-complete.

mercredi 1er mars Bat A29 Amphi G :

  • 14h : Natacha Javerzat Start Heuristics in Mixed-Integer Programs (MIPs)from Timo Berthold’s thesis
    • Résumé : Les Mixed-Integer Programs (MIPs) sont des programmes linéaires dans lesquels certaines variables de décision doivent être des nombres entiers. Alors que la résolution d'un programme linéaire ordinaire est polynomiale, la résolution d'un MIP est NP-difficile. Cependant, résoudre efficacement les MIPs est d'un intérêt immédiat, car leurs applications sont très nombreuses. Pour accélérer les algorithmes de résolution des MIPs, il est crucial de trouver rapidement une "première solution réalisable" qui soit de bonne qualité : cela permet d'élaguer efficacement l'arbre de recherche par la suite en ignorant les branches sous-optimales. C'est l'objet du chapitre 3 "Start Heuristics" de la thèse de Timo Berthold (2006), que nous allons présenter, après quelques rappels sur la programmation linéaire et une introduction aux MIPs. En particulier, nous décrivons et comparons les performances de telles heuristiques, qui sont actuellement utilisées dans des solveurs comme SCIP. (https://scipopt.org/)
  • 14h45 : Dimitrios Periphanos Learning Invariants using Decision Trees and Implication Counterexamples
    • Résumé : L'article présente une méthode pour trouver des invariants de programmes (Utile pour faire de la vérification logicielle) avec une méthode itérative qui met en apprends au fur et à mesures des itérations, à chaque fois le learner propose un invariant et le teacher lui renvoie un contre-example alors en prenant en compte ce nouvel example le learner va trouver un nouvel invariant et ainsi de suite jusqu'à ce que l'invariant soit valide
  • 15h30 : Maximino Bogado Garcia Composable Security of Generalized BB84 Protocols Against General Attacks
    • Résumé :L'article donne une preuve de sécurité de BB84, un protocole de distribution quantique de clés de chiffrement, ainsi que d'autres variantes de ce protocole. Les preuves portent sur la sécurité inconditionnelle du protocole, c'est-à-dire la garantie qu'une tierce personne disposant de tous les outils possibles pour intercepter des informations ne puisse pas retrouver la clé echangée.
  • 16h15 : Edgar Baucher Isometric universal graphs
    • Résumé : Presentation of what are the isometric universal graphs, and some typical problems/questions about them. After that, it will focuses on the open question of the smallest isometric universal graph for trees.