
– Co-directeur de thèse : Xavier LORCA Directeur centre Génie Industriel à IMT Mines Albi-Carmaux
– Encadrant de thèse : Gilles SIMONIN Maître de conférences à IMT Atlantique
L’Université de Nantes et le Laboratoire des Sciences du Numérique de Nantes (LS2N) vous proposent une demi-journée autour de l’entrepreneuriat, du numérique et de la mixité. Ouvert à tous.tes (tous cursus et niveaux confondus).
Proposition de 2 ateliers par le jeu :
A l’issue des ateliers, les participant.e.s seront invité.e.s à échanger autour d’un moment convivial !
Après le monde de l’aléatoire traité en 2019, c’est celui des algorithmes qui sera le thème du Calendrier Mathématique 2020.
Chaque
jour, excepté les week-ends, une question de mathématique à résoudre.
Au fil des mois, un algorithme est présenté à travers une magnifique
illustration enrichie d’un texte explicatif.
Les réponses sont fournies en dernière page du calendrier et présentées de façon détaillée dans le livret des réponses, offert avec le calendrier.
Ana Rechtman Bulajich est maître de conférences en mathématiques à l’université de Strasbourg. Chercheuse engagée dans la promotion des mathématiques, elle souhaite, en parallèle à sa carrière universitaire, faire partager son plaisir de faire des maths. Elle a ainsi participé à la création du concept du Calendrier mathématique édité au Mexique depuis 2002 et en a proposé son adaptation en France.
Exercices (traduction) : Maxime Bourrigan, Pierre Dehornoy, Nicolas Hussenot Desenonges, Sylvain Porret-Blanc, Marion Senjan, Denis Staub.
Textes de Serge Abiteboul, et de Charlotte Truchet.
Les prochaines journées annuelles du GT Vérif auront lieu du 17 au 19 juin 2019 au bâtiment S sur le site de Centrale Nantes.
Elles visent à rassembler la communauté française en vérification formelle, et en particulier les chercheurs juniors, doctorants et post-doctorants, avec pour objectif de favoriser les collaborations et l’ouverture sur des thématiques liées à la vérification. Les domaines inclus sont :
Pour plus d’infos, voir le site http://gt-verif.loria.fr/Wiki.jsp?page=JA-2019
L’équipe TASC du LS2N est heureuse d’accueillir le professeur Peter Van Roy, de l’Université Catholique de Louvain (Belgique).
Ce dernier animera un séminaire en anglais relatif au système de programmation Lasp : « Lasp: Elements of a programming language for edge computing »
vendredi 8 mars 2019 à 9h, dans la salle 3, au RDC du bâtiment 11 du LS2N, sur le site de la Faculté des Sciences et Techniques de Nantes (arrêt de tram : Michelet Science).
Abstract: The Internet is turning inside out: the edge (e.g., mobile networks and Internet of Things) is growing exponentially and the center (data centers) is stable. In a few years, most of the Internet will be at the edge. This poses the question: how do we develop applications to run on edge networks? These networks are highly dynamic with unreliable nodes and intermittent connectivity. In our approach, we consider that these properties are inherent and that edge networks will always be unreliable. Our approach combines convergent computation with hybrid gossip. Convergent computation implements consistent replicated data on unreliable distributed systems. It starts with convergent data structures (CRDTs: Conflict-Free Replicated Data Types) and builds applications by composing them. Hybrid gossip algorithms, such as Plumtree and HyParView, provide a communication layer that maintains connectivity even when 70% or more of nodes fail. The result is the Lasp language and system. Lasp looks to the programmer like a combination of streaming dataflow and functional programming. In this talk, we explain the problems of edge computing and we present Lasp as a first step towards solving them. We give the semantics of Lasp in Sebastien Burckhardt’s abstraction execution formalism. Lasp is so far implemented as a library in Erlang, but eventually it will become a standalone language. We show that the functional approach is well-adapted to edge networks. We have only scratched the surface of this programming style, and we give an overview of the challenges that remain.
***********
The TASC team of the LS2N lab is honored to welcome Professor Peter Van Roy (Université Catholique de Louvain, Belgium) who will present his research in English on « Lasp: Elements of a programming language for edge computing«
Friday, 8 of March at 9 am.
Room 3, building 11, FST site (Michelet Science tram stop)
L’équipe TASC a le plaisir de recevoir le professeur Kazunori Ueda (Université de Waseda, Japon) au LS2N qui fera une présentation en anglais sur
« Analyzing and Understanding Nondeterministic Systems with LMNtal and LaViT »
jeudi 7 mars 2019 à 10h, en salle 3 au RDC du bâtiment 11, sur le site FST .
Abstract:
This talk is a gentle introduction to state-space search and model checking with LMNtal and LaViT, an IDE for LMNtal powered by visualizers.
LMNtal is a language model based on hierarchical graph rewriting that uses point-to-point links to represent connectivity and membranes to represent hierarchy. LMNtal was designed to be a substrate language of various computational models, especially those addressing concurrency, mobility and multiset rewriting. It has close connections with Colored Petri Nets, Interaction Nets, Chemical Abstract Machines, Constraint Handling Rules and Bigraphs. The expressive power of the language was demonstrated through the encoding of diverse computational models including the strong lambda calculus.
Our publicly available LMNtal implementation has evolved into a parallel LTL model checker. The strengths of our LMNtal model checker are its powerful data structures with an inherent symmetry reduction mechanism, highly nondeterministic computation it can express, and little discrepancy between programming and modeling languages. The
implementation achieved high scalability on shared-memory machines and enabled us to handle models with more than a billion states.
The visualizer of the LaViT IDE turned out to be extremely useful in understanding models by state space browsing, which is in sharp contrast with other black-box model checkers. The talk will be given with live demos of examples taken from the fields of model checking, concurrency and AI search.
Ekaterina Arafailova, doctorante au sein de l’équipe TASC, soutiendra sa thèse intitulée « Functional Description of Sequence Constraints and Synthesis of Combinatorial Objects »
mardi 25 septembre 2018 à 14h30 à l’IMT Atlantique dans l’amphi Besse.
La soutenance aura lieu en Anglais. / The defence will be in English and will take place on Tuesday, on the 25th of September, at 14h30, at IMT Atlantique (Nantes) in the Besse amphitheatre.
Jury : Nicolas Beldiceanu (directeur), Rémi Douence (co encadrant), Michela Milano (Rapporteur, Università di Bologna, Bologne, Italie), Stanislav Zivny (Rapporteur, University of Oxford, Oxford, Royaume-Uni), John Hooker (Carnegie Mellon University, Pittsburgh, États-Unis), Claude Jard
Résumé :
À l’opposé de l’approche consistant à concevoir au cas par cas des contraintes et des algorithmes leur étant dédiés, l’objet de cette thèse concerne d’une part la description de familles de contraintes en termes de composition de fonctions, et d’autre part la synthèse d’objets combinatoires pour de telles contraintes. Les objets concernés sont des bornes précises, des coupes linéaires, des invariants non-linéaires et des automates finis ; leur but principal est de prendre en compte l’aspect combinatoire d’une seule contrainte ou d’une conjonction de contraintes. Ces objets sont obtenus d’une façon systématique et sont paramétrés par une ou plusieurs contraintes, par le nombre de variables dans une séquence, et par les domaines initiaux de ces variables. Cela nous permet d’obtenir des objets indépendants d’une instance considérée. Afin de synthétiser des objets combinatoires nous tirons partie de la vue déclarative de telles contraintes, basée sur les expressions régulières, ansi que la vue opérationnelle, basée sur les automates à registres et les transducteurs finis. Il y a plusieurs avantages à synthétiser des objets combinatoires par rapport à la conception d’algorithmes dédiés : 1) on peut utiliser ces formules paramétrées dans plusieurs contextes, y compris la programmation par contraintes et la programmation linéaire, ce qui est beaucoup plus difficile avec des algorithmes ; 2) la synergie entre des objets combinatoires nous donne une meilleure performance en pratique ; 3) les quantités calculées par certaines des formules peuvent être utilisées non seulement dans le contexte de l’optimisation mais aussi pour la fouille de données.
Mots- clés : programmation par contraintes, automates, transducteurs, expressions régulières, séries temporelles, objets combinatoires paramétrés, invariants linéaires et non-linéaires
*********
Abstract:
Contrary to the standard approach consisting of introducing ad hoc constraints and designing dedicated algorithms for handling their combinatorial aspect, this thesis takes another point of view. On the one hand, it focusses on describing a family of sequence constraints in a compositional way by multiple layers of functions. On the other hand, it addresses the combinatorial aspect of both a single constraint and a conjunction of such constraints by synthesising compositional combinatorial objects, namely bounds, linear inequalities, non-linear constraints and finite automata. These objects are obtained in a systematic way and are not instance-specific: they are parameterised by one or several constraints, by the number of variables in a considered sequence of variables, and by the initial domains of the variables. When synthesising such objects we draw full benefit both from the declarative view of such constraints, based on regular expressions, and from the operational view, based on finite transducers and register automata.
There are many advantages of synthesising combinatorial objects rather than designing dedicated algorithms: 1) parameterised formulae can be applied in the context of several resolution techniques such as constraint programming or linear programming, whereas algorithms are typically tailored to a specific technique; 2) combinatorial objects can be combined together to provide better performance in practice; 3) finally, the quantities computed by some formulae can not just be used in an optimisation setting, but also in the context of data mining.
Keywords: constraint programming, automata, transducers, regular expressions, time series, parameterised combinatorial objects, linear and non-linear invariants
Le 14 décembre 2017, Florian Richoux (équipe TASC) a animé la conférence de clôture du cycle sur l’IA proposé par Stéréolux.
Un soixante de personnes s’étaient déplacés pour assister à cette présentation d’un peu plus d’une heure. Les avenirs possibles et impossibles de l’IA dans 10 ans d’un point de vue scientifique et technique ont été abordés. Florian a également parlé d’IA, d’art et de créativité : ce que l’on arrive à faire aujourd’hui et vers quoi on tend certainement. Une conclusion assez large a permis de lancer des questions autour de l’IA dans la société (éthique, droit, travail, etc).
Retouvez :
Charlotte Truchet soutiendra son Habilitation à Diriger des Recherches, intitulée « Vers une programmation par contraintes moins contrainte, outils venant de l’Interprétation Abstraite et de l’Analyse en Moyenne pour définir des solveurs plus expressifs et faciles à utiliser »
jeudi 30 novembre 2017 à 10h, sur le site de la FST.
Jury : Nadia Creignou (Aix-Marseille Université – rapporteure), Christian Schulte (KTH, Suède – rapporteur), Pascal Van Hentenryck (University of Michigan, USA – rapporteur), Gérard Assayag (IRCAM), Frédéric Benhamou (Université de Nantes), Eric Goubault (Ecole Polytechnique), Thomas Jensen (INRIA), Brigitte Vallée (CNRS).
Le manuscrit est disponible en ligne (lien pdf).
En conclusion du cycle, cette conférence abordera les développements à venir de l’intelligence artificielle, aussi bien au niveau technologique que créatif.
Une première intervention proposera un regard prospectif sur les développements technologiques et scientifiques à venir dans le champ de l’intelligence artificielle, et les problématiques techniques et conceptuelles qu’ils poseront. Elle présentera les futures évolutions de ces technologies, et ouvrira de nouvelles pistes de réflexions sur le devenir de l’intelligence artificielle, de ses applications et de ses impacts.
Une deuxième intervention abordera les évolutions à venir dans le champ de l’art et du design, en lien avec les évolutions de l’intelligence artificielle prévues dans un futur proche. Elle permettra de revenir sur les principaux enjeux abordés pendant le cycle, et d’esquisser de nouvelles formes d’interactions entre artistes, designers, intelligences artificielles et publics.
Intervenants : Florian Richoux (équipe TASC), Sylvie Tissot
Plus d’infos sur le site de Stéréolux