Stages proposés 89 sujets à ce jour  

SL308-4 Growing Complex Networks via quantum rules  
Encadrement  
Encadrant : Giuseppe DI MOLFETTA(écrire)
Labo/Organisme : LIS UMR7220
Ville : Marseille

Description  
Complex networks are discrete structures that model a large variety of real systems, from natural to socioeconomic phenomena, such as the protein-protein interaction, the brain, the internet and the international trading. This project merges the field of complex networks (CNs) with the most recent developments in quantum information (QI); two of the raising forces of the information era. Quantum CNs (QCNs), are networks where each vertex and possible link is associated with a quantum state. The dynamics over them is unitary, following the standard quantum mechanical postulates.
The main motivation to understand and model QCNs, as opposed to studying regular quantum lattices, is at least threefold : (i) non-trivial topologies possesses useful properties such as a great robustness to random errors; (ii) recently experimental and theoretical
researchers have understood the importance of QCNs to model the discrete dynamics and geometrical structure of natural phenomena at quantum scale, such as protein folding in DNA, light energy
harvesting in photosynthesis and even emergent
quantum gravity, and (iii) foreseeing the quantum
web. Although recent, there is a variety of theoretical
studies on QCNs, but almost none on their dynamical aspects and their growth. The core idea of this proposal is to contribute to fulfill this theoretical gap and focus on growing QCNs (GQCNs). Our research project makes key contributions to three big questions: How GQCNs can be mathematically modeled? Which are the quantum counterparts of the well-known classical phenomena in large CNs, such as percolation, clustering or small-world topologies? All these questions spread across the foundations of computer sciences and mathematics and have as final goal to refine and implement general mathematical results on several specific model of GQCNs.

Accéder au sujet détaillé

Remarques:
Co-encadrement: Filippo Miatto, ParisTech


SL308-5 Quantum Walks upon irregular graphene-like material  
Encadrement  
Encadrant : Giuseppe DI MOLFETTA (écrire)
Labo/Organisme : LIS UMR 7020
Ville : Marseille

Description  
Quantum walks. QWs are dynamics having the following characteristics: (i) the state space is restricted to the one
particle sector (a.k.a. one ‘walker’); (ii) spacetime is discrete; (iii) the evolution is unitary; (iv) the evolution is homogeneous,
that is translation-invariant and time-independent, and (v) causal (a.k.a. ‘non-signalling’), meaning that information propagates
at a strictly bounded speed. Their study is blossoming, for two parallel reasons.
One reason is that a whole series of novel Quantum Computing algorithms, for the future Quantum Computers, have been
discovered via QWs, or are better expressed using QWs, e.g the Grover search. In these QW-based algorithms, the
walker usually explores a graph, which is encoding the instance of the problem. No continuum limit is taken.
The other reason is that a whole series of novel Quantum Simulation schemes, for the near-future simulation devices, have been
discovered via QWs, and are better expressed as QWs. Recall that quantum simulation is what motivated Feynman to
introduce the concept of Quantum Computing in the first place. Whilst an universal Quantum Computer remains out-ofreach
experimentally, more special-purpose Quantum Simulation devices are seeing the light, whose architecture in fact often
resembles that of a QW. In these QW-based schemes, the walker propagates on the square lattice, and a continuum limit
is taken to show that this converges towards some well-known physics equation that one wishes to simulate. As an added bonus,
QW-based schemes provide: 1/ stable numerical schemes, even for classical computers—thereby guaranteeing convergence
as soon as they are consistent; 2/ simple discrete toy models of the physical phenomena, that conserve most symmetries
(unitarity, homogeneity, causality, sometimes even Lorentz-covariance —thereby providing playgrounds to discuss foundational
questions in Physics. It seems that QWs are unraveling as a new language to express quantum physical phenomena.

Accéder au sujet détaillé

Remarques:
Co-Encadrement: Pablo Arrighi


SL308-10 Recherche de chemins dans un graphe pour la modélisation 3D de complexes protéine-ARN  
Encadrement  
Encadrant : Isaure CHAUVOT DE BEAUCHENE(écrire)
Labo/Organisme : LORIA
Ville : Nancy

Description  
**************************************
Context
**************************************

Le docking consiste à modéliser un assemblage moléculaire à partir de la structure 3D de chaque molécule, par échantillonnage des positionnements relatifs possibles et évaluation de l'énergie d'interaction pour identifier la pose la plus stable.

Les ARN étant hautement flexibles, ils ne peuvent pas être considérés comme rigide au cours du docking. Nous avons donc développé une méthode de docking d'ARN par assemblage combinatoire de fragments (cf hal-01573352 et hal-01925083):

_La séquence d'ARN est coupée en motifs chevauchants
_Chaque motif est associé à un ensemble de fragments 3D possibles
_Les fragments sont dockés sur la protéine et les poses de meilleure score sont retenues
_Les poses spatialement adjacentes sont assemblés en une chaine d'ARN de sequence souhaitée
_Les chaines de plus basse énergie totale sont sélectionnées

[Schema: https://tinyurl.com/ycsj6n63]

**************************************
Objectifs
**************************************

L'assemblage des poses de fragments en chaines d'ARN correspond à une recherche de chemin de plus basse énergie dans un graphe orienté représentant la connectivité 2-à-2 des poses. Le but de ce stage est de passer d'une recherche de chemin brute force et exacte à une recherche probabiliste. Nous ajouterons pour cela des pondérations aux sommets (i) et arêtes (ii) du graphe:

(i) La proximité spatiale de 2 poses sera transformée en une probabilité de connection, au lieu du critère binaire utilisé actuellement.

(ii) Chaque pose sera pondérée par la somme de son énergie d'interaction avec la protéine et son énergie de conformation interne (nous utiliserons pour calculer ces energies des outils existants)

**************************************
Stratégie
**************************************

Le travail consistera en :

_l'étude du papier et du rapport décrivant la méthode d'assemblage des poses.
_la prise en main des outils d'assemblage existants.
_le calcul des énergies internes des fragments par un outils existant (e.g. AMBER)
_la comparaison des distances inter-pose entre vrai et faux positifs dans les paires de poses.
_le choix d'une fonction transformant cette distance en probabilité de connection
_l'implementation de cette fonction et des énergies calculées dans les outils d'assemblage.
_la validation du nouvel outils d'assemblage sur des cas déjà testé avec la méthode actuelle.

La méthode sera testée sur un grand nombre de cas de structures 3D de complexes ARN-protéine connues expérimentalement. Ce travail devrait permettre d'échantillonner plus efficacement les structures possibles de chaines d'ARN.


Remarques:
**************************************
Modalités de stage
**************************************
Le stage pourra être rémunéré sous forme de gratification et/ou d’hébergement en chambre universitaire.
Il sera co-encadré par Antoine Moniot, doctorant dans l’équipe sur le docking ARN-protéine

**************************************
Equipe d'accueil
**************************************

L'équipe CAPSID (dir. David Ritchie), au Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA, CNRS - INRIA – UL, à Nancy), développe des outils de modélisation 3D et simulation numérique des assemblages moléculaires à l'échelle atomique.
Nos recherches combinent biophysique, biologie structurale et algorithmique appliqué aux coordonnées 3D, aux graphes, au clustering et à l'apprentissage automatique.
Nos outils sont développés et appliqués en étroite collaboration avec plusieurs équipes expérimentales de biologie/biophysique.

**************************************
Compétences requises
**************************************

Solides connaissances en algorithmique, analyse de graphe, combinatoire, statistiques
Solides compétences en programmation python


SL308-11 Optimisation d'une fonction de score pour la modélisation 3D de complexes protéine-ARN  
Encadrement  
Encadrant : Isaure CHAUVOT DE BEAUCHENE(écrire)
Labo/Organisme : LORIA
Ville : Nancy

Description  
Mots-clef: Apprentissage statistique, Bioinformatique, Modélisation Moléculaire.

**************************************
Context
**************************************

Le docking consiste à modéliser un assemblage moléculaire à partir de la structure 3D de chaque molécule, par échantillonnage des positionnements relatifs possibles et évaluation de l'énergie d'interaction pour identifier la pose la plus stable.
Nous avons récemment développé une méthode de docking des ARN simple-brin par assemblage combinatoire de fragments d'ARN: les fragments sont dockés sur la surface de la proteine, les poses de meilleurs scores sont retenues pour etre ensuite assemblées en une chaine continue d'ARN (cf hal-01573352 et hal-01925083).

[Schema: https://tinyurl.com/ycsj6n63]

La principale limite de la méthode est la fonction de score, qui est trop imparfaite pour sélectionner les meilleures poses (position et orientation) des fragments sans garder trop de faux positifs.


**************************************
Objectifs
**************************************
Le but de ce stage est d'optimiser la fonction de score pour le docking protéine-ARN. Dans un positionnement donné des 2 molécules, cette fonction calcule la somme des énergies d'interations pour chaque paire d'atome ARN - protéine. Chaque énergie d'interaction atome-atome est une fonction de la distance atome-atome et du type de chaque atome (rayon, charge partielle ...). Elle contient deux paramètres variables pour chaque paire de type d'atome donnée, qui décrivent leur distance optimale et l'énergie à cette distance optimale.
Ces deux paramètres seront optimisés par apprentissage automatique sur un large ensemble de structures 3D de complexes ARN - protéine connues expérimentalement.


**************************************
Stratégie
**************************************
Nous avons defini une stratégie d'apprentissage acceleré, qui s'appuie partiellement sur les travaux de [A. Sasse et al (2017) PloS one 12(1)e0170625]. Le travail consistera en :

• l'étude de la méthode d'apprentissage accélérée et la prise en main des outils associés
• la production et l'organisation de résultats de docking de fragments (outils existants)
• l'automatisation de l'apprentissage sur un grand nombre de cas d'entrainement.
• l'analyse des résultats obtenue par différents runs indépendants d'apprentissage.
• la validation des nouvelles fonctions de score sur des cas test.

L'utilisation de la fonction de score optimisée devrait permettre d’enrichir en poses correctes l'ensemble des poses sélectionnées pour faire l'assemblage en chaine d'ARN. De plus, cette fonction de score sera mise à disposition de la communauté de bio-informatique en tant que
premiere fonction de score existante qui soit spécifique des ARN simple-brin.

Remarques:
**************************************
Modalités de stage
**************************************
Le stage pourra être rémunéré sous forme de gratification et/ou d’hébergement en chambre universitaire.

Il sera co-encadré sur la partie docking par Antoine Moniot, doctorant dans l’équipe.

**************************************
Equipe d'accueil
**************************************

L'équipe CAPSID (dir. David Ritchie), au Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA, CNRS - INRIA – UL, à Nancy), développe des outils de modélisation 3D et simulation numérique des assemblages moléculaires à l'échelle atomique.
Nos recherches combinent biophysique, biologie structurale et algorithmique appliqué aux coordonnées 3D, aux graphes, au clustering et à l'apprentissage automatique. Nos outils sont développés et appliqués en étroite collaboration avec plusieurs équipes expérimentales de biologie/biophysique.

**************************************
Compétences requises
**************************************

Solides connaissances en apprentissage statistique
Solides competences en programmation python


SL308-13 Transformées en cosine et sine discrètes pour futur standard de compression vidéo  
Encadrement  
Encadrant : Wassim HAMIDOUCHE(écrire)
Labo/Organisme : IETR VAADER Team
Ville : Rennes

Description  
L’objectif de ce stage est d’approximer
ces trois transformées (DCT-V, DCT-VIII et DST-VII) à partir de la DCT-II et DST-I et d’autres matrices creuses pour réduire le nombre de multiplications et d’additions d’une multiplication matricielle. Cette solution permettra aussi de réduire les ressources matérielles (espace mémoire et calcul) pour une implémentation temps réel sur une plateforme embarquée type FPGA.
Ce projet se déroule en quatre étapes qui consistent à :

1. Faire un état de l’art sur les transformées DCT et DST [1, 2] (bibliographie) – [2 semaines].

2. Modélisation théorique de l’approximation sous la forme d’un problème d’optimisation avec contraintes – [4 semaines].

3. Utilisations des méthodes d’optimisation non linéaires pour résoudre le problème d’optimisation. Et trouver des approximations aux transformées DCTV, DCT-VIII et DST-VII) basées sur les transformées DCT-II et DST-I [4 semaines].

4. Évaluer les performances des solutions proposés en terme de d’erreur et d’orthogonalité, rédaction du rapport du stage. [2-4 semaines].

Accéder au sujet détaillé

Remarques:
Stage remuniré par une gratification de 577 euos par mois plus la possibiltè de prise en charge du logement dans la résidence INSA Rennes.


SL308-14 Combining Solvers for Test Data Generation  
Encadrement  
Encadrant : Yvan LABICHE(écrire)
Labo/Organisme : Carleton University, Dept. SCE
Ville : Ottawa, Canada

Description  
During black-box testing a test case is derived from a specification as a set of actual (test input) values. For instance, when testing a software that returns the location of the first occurrence of a character in a string, a test case could consist of providing string “abcdbgef” and character ‘b’ (the software should return value 2). We developed tool support for a black-box testing technique that produces abstract test cases, i.e., test case specifications. These are test case specification, not test cases, since they only provide a specification of what the test input data should look like instead of the actual test input data. An abstract test case provides a specification such as, in the case of the character search example above: the input string shall have more than two characters, the character shall appear more than once, and its first occurrence shall not be at the first position. (Notice the test case above, with input values “abcdbgef” and ‘b’, conforms to this test case specification.) Fortunately, our technology provides test case specifications in an electronic form, which can be processed automatically to identify test input data that conform to those test case specifications. To automatically identify test input data that conform to such test case specifications we intend to use SAT and/or SMT technologies such as Microsoft’s Z3 solver. Satisfiability (SAT) is the problem of identifying whether there exists a solution to a given Boolean formula. An extension of SAT is Satisfiability Modulo Theory (SMT), whereby the problem to be solved is not restricted to Boolean clauses but can also involve integers and real numbers, arrays, or even strings. Different SAT and SMT solvers exist; they have their pros and cons, support different types, to different extent. There is no silver bullet and no single solver will be able to generate, in a large number of situations, test case data from test case specifications; different solvers will need to work hand in hand. The project is to identify (short literature review) which solvers can theoretically work together and whether they can practically work together (engineering solution). The solution will be integrated in our tool infrastructure and the research will include experiments whereby the black-box testing technique will be used on several case studies.

Remarques:
Students will be offered a modest research stipend to cover living expenses and travel costs associated with this project.
Students will also have access to all campus services and facilities including the library, athletics complex, etc. Access to
on-campus accommodations may also be available.


SL308-15 A Formal Semantics of SIMD Instruction Sets  
Encadrement  
Encadrant : Pierre-Evariste DAGAND(écrire)
Labo/Organisme : LIP6 - Inria
Ville : Paris

Description  
As part of the [Usuba](https://github.com/DadaIsCrazy/usuba) project, we produce efficient cryptographical code, exploiting various SIMD (Single Instruction, Multiple Data) instruction sets such as SSE, AVX, AVX2 or AVX512 on [Intel platforms](https://software.intel.com/sites/landingpage/IntrinsicsGuide). Aside from producing high-performance code, Usuba also aims at being a trustworthy compiler: we would like to prove that the generated code follows the semantics prescribed by the input program. To this end, we need to have a formal semantics of SIMD instructions in our favorite proof assistant, Coq.

This project offers to:
- give a Coq semantics to a significant subset of the SSE and AVX instruction sets, using as many generic programming tricks as possible to keep the model as concise as possible;
- develop an automated testing infrastructure, allowing us to exercise the formal semantics against the actual implementations of the instruction set;
- extend the [Jasmin](https://jasmin-lang.github.io/) portable assembler with the instructions supported by our model, updating its correctness proof in the process.


Accéder au sujet détaillé

Remarques:
Possibilité de rémunération à la gratification standard (~500€) pour les auditeurs.


SL308-16 4-coloration des graphes planaires et orientations  
Encadrement  
Encadrant : Daniel GONÇALVES(écrire)
Labo/Organisme : LIRMM
Ville : Montpellier

Description  
Le Théorème des 4 couleurs affirme que toute carte peut être coloriée avec 4 couleurs, de façon à ce que des régions voisines aient des couleurs différentes. Il a fallu plus d’un siècle pour montrer ce résultat et les seuls preuves connues font appel à un programme de vérification. Dis autrement, aucun être humain n’a vérifié à la main
chaque étape de ces preuves.

Le but de ce stage est de vérifié expérimentalement l'hypothèse suivante :

Tout graphe planaire 5-connexe vérifie le critère de Alon-Tarsi pour la 4-colorabilité.

Cette vérification sur de petits graphes, si elle s'avère positive, guidera la recherche d'une preuve formelle de l'hypothèse.

Accéder au sujet détaillé

Remarques:
Encadrants :
Daniel Gonçalves daniel.goncalves@lirmm.fr
Petru Valicov petru.valicov@lirmm.fr

Rémunération : Indemnité standard des stages.

N’hésitez pas à nous contacter pour des questions ou tout simplement pour plus de détails !


SL308-18 Positive systems, Newton, games, and convergence  
Encadrement  
Encadrant : Elias TSIGARIDAS(écrire)
Labo/Organisme : LIP6
Ville : Paris

Description  
General description.
One of the most important problems in the theory of infinite-state recursive probabilistic systems, like for example stochastic, context-free grammars, is the computation of the terminating probabilities. This is equivalent to compute the least fixed point solution of a positive polynomial system [1,2]. A positive polynomial system is a system that has equations of the form $x_i = P_i(x_1,...,x_n)$, where $i$ is a number in $1,...,n$ and $P_i$ is a multivariate polynomial with only positive coefficients.

Objectives.
The known algorithms for computing the least fixed point solution of a positive polynomial system, when such point exists, are based on an application of Newton application and they have linear convergence. The objective of the internship is to survey on the known algorithms, analyse carefully their Boolean complexity, and introduce a Newton operator with quadratic convergence based on recent developments in computational algebra [3].


Bibliography
1. J. Esparza, S. Kiefer, and M. Luttenberger. Computing the least fixed point of positive polynomial systems. SIAM Journal on Computing, 39(6):2282-2335, 2010.
2. A. Stewart, K. Etessami, and M. Yannakakis.Upper bounds for Newton’s method on monotone polyno- mial systems,and P-time model checking of probabilistic one-counter automata. Journal of the ACM, 62(4):30, 2015.
3. V. Y. Pan and E. P. Tsigaridas. Nearly Optimal Refinement of Real Roots of a Univariate Polynomial. Journal of Symbolic Computation 74:181-204 2016.

Remarques:
The internship will run under the umbrella of collaboration of Inria, LIP6, and École Polytechnique in the realm of the PGMO grant ALMA. Interested candidates are encouraged to contact Elias Tsigaridas for additional information.


SL308-19 Rust for Performance: Parallel Data Structure for Stream Data Storage.  
Encadrement  
Encadrant : Brnuo RAFFIN(écrire)
Labo/Organisme : INRIA
Ville : GRENOBLE

Description  
The analysis of large multidimensional spatiotemporal datasets poses challenging questions regarding storage requirements and query performance. Several data structures have recently been proposed to address these problems that rely on indexes that pre-compute different aggregations from a known-a-priori dataset. Consider now the problem of handling streaming datasets, in which data arrive as one or more continuous data streams. Such datasets introduce challenges to the data structure, which now has to support dynamic updates (insertions/deletions) and rebalancing operations to perform self- reorganizations. We developed a Packed- Memory Quadtree (PMQ), that efficiently supports dynamics data insertions and outperform other classical data structures like R-trees or B-trees. The PMQ ensures good performance by keeping control on the density of data that are internally stored in a large array. The PMQ is based on the Packed Memory Array [3,4,5] and share with it its amortized cost of O(log^2(N)) per insertion. But today all processors are multicores. Data structures need to be parallelized to leverage the compute power available. The goal of this internship is to design, develop and test a parallel version of the PMQ using the Rust programming language (or C++).

Accéder au sujet détaillé

Remarques:
INRIA team Datamove - Co-advised with Frederic Wagner


SL308-21 Interference analysis for the new Kalray MPPA3 many-core  
Encadrement  
Encadrant : Claire MAIZA(écrire)
Labo/Organisme : Verimag/Univ. Grenoble Alpes
Ville : Grenoble (ou Lyon)

Description  
In automotive and avionics, some programs are subject to critical timing constraints.
In these real-time critical systems, the timing properties must be guaranteed.
Among them, the worst-case execution time that guarantees an upper-bound on the execution time of programs.
On a multi-core platform, this worst-case execution is highly influenced by all concurrent programs.
In our work, we studied the Kalray MPPA2 platform (a set of multi-core communicating through a network on chip comprising 256 compute cores, designed by a company located in Montbonnot, near Grenoble), and designed an algorithm able to tightly bound the interference, taking into account both the specificities of the software application and the low-level details of the hardware architecture.
Our interference analysis models the interference on the memory bus and the communications through the network-on-chip.
In the new generation of chip, the MPPA3 (announced in 2017), considerable changes have been made to the architecture (less clusters but faster communications and memory access). The generic part of our algorithm are still valid, but the mathematical model of the hardware architecture must be redesigned.
The goal of the internship is to analyze how far our previous work may be adapted to this new platform and propose modified/new interference analysis.

Remarques:
Ce sujet est co-encadré par Matthieu Moy au LIP à Lyon. Le stage peut se dérouler à Lyon ou Grenoble.


SL308-22 Scalability of the interference analysis for a multi-core platform  
Encadrement  
Encadrant : Claire MAIZA(écrire)
Labo/Organisme : Verimag/Univ. Grenoble Alpes
Ville : Grenoble (ou Lyon)

Description  
In automotive and avionics, some programs are subject to critical timing constraints.
In these real-time critical systems, the timing properties must be guaranteed.
Among them, the worst-case execution time that guarantees an upper-bound on the execution time of programs.
On a multi-core platform, this worst-case execution is highly influenced by all concurrent programs.
In our work, we studied the Kalray MPPA2 platform (a set of multi-core communicating through a network on chip comprising 256 compute cores, designed by a company located in Montbonnot, near Grenoble), and designed an algorithm able to tightly bound the interference.
Our interference analysis models the interference on the memory bus and the communications through the network-on-chip.
This analysis showed very good results in terms of precision, but is limited in terms of scalability (the overall algorithm is O(n^4) in number of tasks). We already have ideas on how to reduce the complexity and improve the scalability (by changing the way we iterate to find a solution), and on how to improve the precision further (through a better study of the communication, memory accesses and scheduling).The aim of this internship is to explore one of the improvement axis and implement it in our analysis tool.

Remarques:
Ce sujet et co-encadré par Matthieu Moy au LIP. Le stage peut se dérouler à Grenoble ou à Lyon.


SL308-23 Combinations of cache analyses  
Encadrement  
Encadrant : Claire MAIZA(écrire)
Labo/Organisme : Verimag/Univ. Grenoble Alpes
Ville : Grenoble

Description  
Cache memory are generally used to gain memory access efficiency. They are small and fast memories close to the processor. They are limited in size and are used as buffer to temporary contain data or instruction with fast access.
Cache analysis is used in safety and security context, for instance, to guarantee an upper-bound on the execution time or to guarantee that the execution is not vulnerable certain to side channel attacks.
In Verimag, recently, we have developed a new cache analysis (POPL 2019) that is more efficient and complete than Ferdinand’s traditional one.
The objectives of this internship is to study how this new analysis can be combined with others (persistence analysis? partitioning? data analysis? other replacement strategy?).
If possible, analyses will be implemented in our tool (a variant of OTAWA).

Remarques:
Ce sujet est co-encadré par David Monniaux.


SL308-25 Analyse de fréquence d’activation  
Encadrement  
Encadrant : Pascal SOTIN(écrire)
Labo/Organisme : IRIT
Ville : Toulouse

Description  
L'analyse statique du pire temps d'exécution d'un programme requiert la connaissance de limites précises sur le nombre d'itérations de chacune des boucles du programme. Notre équipe développe un outil d’analyse de bornes de boucles qui établit une relation entre le numéro de l’itération et la valeur des variables. Pour obtenir une limite précise au temps d’exécution, il reste à déterminer la quantité de code exécuté par les différentes itérations de la boucle ; par exemple à travers la fréquence d’activation d’une condition.

L'objectif du stage est de proposer une analyse statique permettant de dériver automatiquement une limite sur la fréquence d’activation des conditions contenues dans le corps d’une boucle. On dispose déjà pour cette boucle d’une relation liant la valeur des variables au numéro de l’itération et d’une borne sur le nombre d’itérations.

Une implémentation de l’analyse proposée est attendue. Le langage sera de préférence OCaml, pour un interfaçage facile avec la bibliothèque développée dans l’équipe.


Accéder au sujet détaillé


SL308-26 Synchronisation-free mobile gaming  
Encadrement  
Encadrant : Marc SHAPIRO(écrire)
Labo/Organisme : Sorbonne-Université–LIP6
Ville : Paris

Description  
*Background*
In online multi-player games the inherent challenges of mobile and edge computing are worsened by the requirements of real-time users’ interactions. Thus, developers of such applications face difficult design choices on data storage and distribution that ultimately affect the gaming experience: adopting a weak consistency model across replicas and mobile terminals will expose anomalies to the users, whereas a strong consistency model will increase latency, which may be unacceptable.

To address these issues, we propose to use Antidote and EdgeAnt. Antidote is a data store that provides an adequate consistency semantics with optimal performance by minimizing the need for synchronization between storage replicas. It offers a causally consistent transactional API and a toolkit of convergent data types that accommodates the typical needs of distributed applications. EdgeAnt extends Antidote with a consistent, mutable cache on the Edge device, with the same API and consistency guarantees. With support for client migration, P2P group communication and load placement at the edge or at the datacenter.

*Research objectives and methods*
The aim of this project is to design and develop a simple yet fully-functional gaming application to evaluate the pros and cons of the synchronization-free approach. Besides being an interesting pilot study for online multi-player gaming, this application will allow us to perform a thorough experimental evaluation of Antidote.

We break down the project into the following steps:

Brief study of the state of the art.
Developing a simple, but fully functional, gaming application (e.g. asynchronous command line chess) with the goal of familiarising with the design, deployment and APIs of Antidote.
Adaptating an existing open source multi-player gaming application (e.g. 0.AD) that to use the synchronization-free approach; functional and scalability testing.

Accéder au sujet détaillé

Remarques:
How to apply
The intern must:

Be enrolled’ in Computer Science / Informatics or a related field.
Have an excellent academic record.
Be strongly interested in, and have good knowledge of, distributed systems and/or distributed games.
Be motivated by experimental research.
The internship is funded, and will take place in the Delys group, at Laboratoire d’Informatique de Paris-6 (LIP6), in Paris. It will be advised by Ilyas Toumlilt, Dimitrios Vasilas and Dr. Marc Shapiro. A successful intern will be invited to apply for a PhD.

To apply, contact Ilyas Toumlilt <ilyas.toumlilt@lip6.fr> and Dimitrios Vasilas <dimitrios.vasilas@lip6.fr>, with the following information:

A resume or Curriculum Vitæ.
A list of courses and grades of the last two years of study (an informal transcript is OK).
Names and contact details of two references (people who can recommend you), whom we will contact directly.


SL308-27 Towards Efficient Big Data Management with Transient Storage Systems  
Encadrement  
Encadrant : Gabriel ANTONIU(écrire)
Labo/Organisme : IRISA/Inria Rennes Bretagne Atlantique
Ville : Rennes

Description  
Advisors:

- Gabriel Antoniu, Research director, Inria, gabriel.antoniu@inria.fr (main advisor)
- Nathanaël Cheriere, ENS Rennes, nathanael.cheriere@irisa.fr

Keywords:
HPC, Big Data, data management, distributed storage systems, transient storage systems

Subject:
We live in the era of Big Data. Huge amounts of data are collected from diverse sources, such as sensor arrays, social media, or scientific simulations and other experiments. As data must be analyzed to extract meaningful information, new techniques and tools (such as MapReduce [1]) have recently been developed to manage and process increasingly larger amounts of data at an appropriate speed to meet application requirements.

In the High Performance Computing (HPC) domain, huge amounts of data are collected from complex simulations of physical phenomena (such as climate modeling, galaxy evolution, etc.), and data analysis techniques from the field of Big Data are used to extract pertinent informations. Needless to say, data storage is a cornerstone of Big Data processing. Whereas traditional HPC systems usually separate computational resources from storage, using parallel file systems, new supercomputers now often have local storage devices (such as SSDs or NVRAM) located on their compute nodes. This local storage allows users to deploy new types of distributed storage systems along with the applications. Such a storage system, deployed only for the duration of an application’s execution, is called a transient storage system.

This internship focuses on answering the following research question: "How can we efficiently deploy and terminate a transient storage system?". Indeed, a transient storage system only exists during the run time of the application that uses it, initially hosting no data. When the application terminates, data would be lost if not backed up. Thus, two steps are needed: loading data from the persistent storage at initialization time, and dumping the data onto the persistent storage before termination. Both operations involve large data transfers that may slow down the initialization and termination of such storage systems. Optimizing these transfers would lead to faster application deployments and termination.

Multiple relevant contributions can be achieved during this internship depending on the affinity of the student.

1. Theoretical contributions: establish a lower bound (mathematical model) of the duration of the operations of loading and dumping data in order to identify their bottlenecks, and have a baseline for the evaluation of implementations of such systems. This contribution would be in the continuity of [2] and [3].

2. Algorithmic contributions: optimize the algorithms used to transfer the data between nodes. For instance, one can consider the network topology, or use AI to monitor the application’s behavior and load/dump data in the background.

3. Experimental contributions: implement the algorithms in Pufferbench (a benchmark designed to evaluate commission and decommission algorithms - https://gitlab.inria.fr/Puffertools/Pufferbench) to experiment with the algorithms previously designed.

4. Validation contributions: implement and evaluate a microservice able to efficiently run the studied operations using Mochi (a set of libraries designed to quickly build distributed storage systems - https://www.mcs.anl.gov/research/projects/mochi/).

Transient storage systems often act as caches for distributed applications, similarly to burst buffers [4]. For such a use, a transient storage system should be able to choose which data to load (resp. dump), when to load it, and where to place it. A diverse set of strategies can be used: from "loading everything at start-up" to "loading only when the data is accessed", with more complex approaches using access monitoring and machine learning to predict which data will be needed by the application in the near future. Some of these strategies could be studied depending on the progress and affinities of the student.

This subject will be done in close collaboration with Matthieu Dorier from Argonne National Laboratory (ANL, USA). In addition to the possibility to interact with top-level researchers and scientists from ANL, the work can involve the use of large-scale HPC experimental facilities available at Inria and at ANL.


Accéder au sujet détaillé

Remarques:
Required skills and abilities
C++
Algorithmics
Mathematics
Affinity with distributed storage systems

Bibliography
1. Dean, Jeffrey, and Sanjay Ghemawat. "MapReduce: simplified data processing on large clusters." Communications of the ACM51.1 (2008): 107-113.

2. Cheriere, Nathanaël, and Gabriel Antoniu. "How fast can one scale down a distributed file system?." Big Data (Big Data), 2017 IEEE International Conference on. IEEE, 2017. Available at https://hal.archives-ouvertes.fr/hal-01644928/document

3. Cheriere, Nathanaël, Matthieu Dorier, and Gabriel Antoniu. A Lower Bound for the Commission Times in Replication-Based Distributed Storage Systems. Inria Rennes-Bretagne Atlantique, 2018. Available at https://hal.archives-ouvertes.fr/hal-01817638/document

4. Liu, Ning, et al. "On the role of burst buffers in leadership-class storage systems." Mass Storage Systems and Technologies (MSST), 2012 IEEE 28th Symposium on. IEEE, 2012.


SL308-28 Automated discovery of physico-chemical structures with intrinsically motivated deep learning algorithms.  
Encadrement  
Encadrant : Pierre-Yves OUDEYER(écrire)
Labo/Organisme : Inria Bordeaux Sud-Ouest
Ville : Bordeaux

Description  
Background: Many physical and chemical systems that we encounter are complex and dynamic. For example, the air flow around a rotor blade of a wind turbine can form different turbulence patterns over time. Those dynamics depend on parameters such as the form of the rotator blade, the wind direction and others. The knowledge about the range of dynamics and how they depend on the parameters is helpful, for example to design new rotor blades. Unfortunately, they are often unknown and experiments are needed to uncover them. Conducting such experiments manually is often too time intensive. A solution comes from the application of AI and robotics, which perform and control the exploration of such systems automatically.

The project: The internship will be part of a project investigating the usage of intrinsically motivated goal exploration algorithms for the exploration of physical and chemical systems. This new family of algorithms use goal spaces about their target systems. The goal space defines goals that the agent might want to achieve, for example to produce a certain turbulence pattern. The agent self-generates its own goals from the goal space based on principles of intrinsic motivation that are inspired by human cognitive development (Deci and Ryan, 1985). The agent then explores and learns which system parameters achieve the generated goals.
The framework has been shown to allow real world robots to efficiently acquire skills such as tool use in high-dimensional continuous state and action spaces (e.g. Baranes and Oudeyer, 2013; Forestier et al., 2016). In the domain of chemistry and physics, they opened the possibility to automate the discovery of novel chemical or physical structures produced by complex dynamical systems (e.g. Grizou, Points et al., 2018, https://croningp.github.io/tutorial_icdl_epirob_2017/ ).
However, previous approaches have assumed that self-generated goals are sampled in a specifically engineered feature space, limiting their autonomy. Recent work has shown how unsupervised deep learning approaches could be used to learn goal space representations (e.g. Péré et al., 2018), but they focused on goals represented as static target configurations of the system.
In this project, we investigate how goal space representations for dynamical systems can be learned based on raw sensory observations, for example video camera images. The goal is to enable intrinsically motivated goal exploration algorithms to autonomously discover new and interesting behaviors of dynamical systems.

Your contribution: As part of this project you will implement and test methods to learn goal spaces for dynamical systems. Methods will be based on deep neural networks (LeCun et al., 2015), and more particularly learning recurrent generative models, used to learn a latent representation of the dynamics in a system. As application scenarios will be simulated systems used such as cellular automata. Python and deep learning libraries such as PyTorch will be used to implement the algorithms.

References:

FLOWERS web site: http://flowers.inria.fr

Baranes, A., & Oudeyer, P. Y. (2013). Active learning of inverse models with intrinsically motivated goal exploration in robots. Robotics and Autonomous Systems, 61(1), 49-73.

Deci E. & Ryan, R. (1985). Intrinsic Motivation and Self-Determination in Human Behavior. Plenum Press.

Grizou, J., Points, L.J., Sharma, A. & Cronin, L. (2018). A Closed Loop Discovery Robot Driven by a Curiosity Algorithm Discovers Proto-Cells That Show Complex and Emergent Behaviours. ChemRxiv. Preprint.

LeCun, Y., Bengio, Y. & Hinton, G. (2015). Deep learning. Nature, 521(7553), 436-444.

Forestier, S., Mollard, Y., Caselli, D. & Oudeyer, P. Y. (2016). Autonomous exploration, active learning and human guidance with open-source Poppy humanoid robot platform and Explauto library. In The Thirtieth Annual Conference on Neural Information Processing Systems (NIPS 2016).

Péré, A., Forestier, S. & Oudeyer, P-Y. (2018) Unsupervised learning of goal spaces for intrinsically motivated goal exploration. In Proceedings of ICLR 2018.




Accéder au sujet détaillé


SL308-30 Numerical Methods for Computing Fundamental Information Theoretic Limits of Communication  
Encadrement  
Encadrant : Malcolm EGAN(écrire)
Labo/Organisme : CITI
Ville : Lyon

Description  
Since Shannon, information theoretic quantities have played a key role in providing fundamental limits of communication. This is true not only in classical communication systems, but also in the wireless networks arising in the Internet of Things. There are two key features of these new IoT networks:
(1) Noise is not always well-modeled by Gaussian processes, and heavy-tailed models (such as alpha-stable) can provide a better fit [1].
(2) Due to the small quantities of data that must be transmitted, short blocklength coding schemes are desirable [2].

Due to the work by Polyanskiy et al [3], there are now general information theoretic bounds available for the maximum achievable rate data that can be communicated with a given probability of error. While these bounds have been extensively studied in discrete and Gaussian noise models, this is not the case for the heavy-tailed noise models arising in IoT.

The goal of this project will be to develop and implement numerical algorithms to compute the information theoretic bounds in point-to-point communication systems with heavy-tailed noise. These algorithms will be based on Monte Carlo approaches, applying variance reduction and rare-event simulation methods. The targeted outcomes of the project are:
(i) An algorithm implemented in MATLAB or Python using standard Monte Carlo estimation for relatively large probabilities of error.
(ii) An efficient algorithm to study the bounds for low probabilities of error using variance reduction methods.
(iii) A numerical study of the information theoretic bounds to investigate the effect of noise parameters on achievable communication rates.

Ideally, the candidate will have a background programming in MATLAB or Python and introductory probability theory (random vectors, probability distributions, expectations). Previous exposure to information theory is desirable but not required.

This project will be primarily supervised by Dr. Malcolm Egan (https://malcolmalexegan.wordpress.com), with co-supervision by Prof. Jean-Marie Gorce and Prof. Philippe Mary. For more information, please contact Dr. Egan (malcom.egan@inria.fr).

[1] Egan, M., Clavier, L., Zheng, C., de Freitas, M. and Gorce, J.-M., “Dynamic interference in uplink SCMA for large-scale wireless networks without coordination,” accepted for publication in EURASIP Journal on Wireless Communications and Networking.

[2] Philippe Mary, Jean-Marie Gorce, Ayse Unsal, H. Vincent Poor
2016 IEEE Global Communications Conference: Workshops: First IEEE International Workshop on Low-Layer Implementation and Protocol Design for IoT Applications , Dec 2016, Washington, DC, United States. 2017

[3] Y. Polyanskiy, H. Poor, and S. Verdu, Channel Coding Rate in the Finite Blocklength Regime, IEEE Transactions on Information Theory, vol.56, issue.5, pp.2307-2359, 2010.

Remarques:
This project will be co-advised by Prof. Jean-Marie Gorce (CITI, Lyon) and Prof. Philippe Mary (INSA Rennes).



SL308-31 Calculabilité dans les espaces topologiques  
Encadrement  
Encadrant : Mathieu HOYRUP(écrire)
Labo/Organisme : Loria
Ville : Nancy

Description  
La théorie de la calculabilité sur les entiers et obtejs finis peut être étendue à des objets infinis, représentés sur le ruban infini d'une machine de Turing. Ce type de calcul est fortement lié à la topologie : par exemple, toute fonction calculable est continue. Ainsi les notions de calculabilité peuvent s'étendre à de nombreux espaces topologiques, une machine pouvant prendre un entrée l'encodage d'un point de l'espace.

Cependant les liens entre calcul et topologie, bien compris pour les espaces simples (à base dénombrable), sont mal compris ailleurs. L'objectif du stage est d'explorer ces liens sur certains espaces particuliers, comme l'espace des polynômes à coefficients réels.

Accéder au sujet détaillé


SL308-32 Geometry and topology of parametric curves  
Encadrement  
Encadrant : Elias TSIGARIDAS(écrire)
Labo/Organisme : LIP6/INRIA
Ville : Paris

Description  
General description.

Let $\mathcal{C}$ be an algebraic curve in $\mathbb{C}^n$, that is the one-dimensional set of solutions of a system of polynomial equations in $n$ variables with complex coefficients.

We call $\mathcal{C}$ a \textit{rational curve}
if there is a map
\[
\label{eq:psi-def}
\psi : t \mapsto
\left( \frac{f_1 (t)}{g_1 (t)},\ldots , \frac{ f_n(t)}{g_n (t)}\right) ,
\]
where the $f_i$'s and the $g_i$'s are univariate polynomials and
$t \in \CC$, so that $\mathcal{C}$ is the Zariski closure of the image of $\psi$. The map $\psi$ is the rational parametrization of $\mathcal{C}$.


There are a lot of results and algorithms concerning the geometry and the topology of curves in the real plane when they are given in implicit form, that is when the curve is given as the real zero-set of a bivariate polynomial $f(x, y) = 0$.
However, very little is known for the topology and the geometry of rational curves $\mathcal{C} \cap \mathbb{R}^n$, with some notable exceptions, e.g., [1].


Objectives.

The objective of the internship is to survey carefully the known tools [2,3,4] for characterizing the (real) singularities of parametric curves in $\mathbb{R}^n$, to develop an algorithm for computing the topology, analyse its complexity, and present a prototype implementation in \textsc{maple}.


Bibliography

[1] Alc\'azar, Juan Gerardo, and Gema Mar\'ia D\'iaz-Toca. ``Topology of 2D and 3D rational curves.'' Computer Aided Geometric Design 27, no. 7 (2010): 483-502.

[2] Rubio, Rosario, J. Miguel Serradilla, and M. Pilar V\'elez. ``Detecting real singularities of a space curve from a real rational parametrization.'' Journal of Symbolic Computation 44, no. 5 (2009): 490-498.

[3] Andradas, Carlos, and Tom\'as Recio. ``Plotting missing points and branches of real parametric curves.'' Applicable Algebra in Engineering, Communication and Computing 18, no. 1-2 (2007): 107-126.

[4] Manocha, D., Canny, J.F., 1992. ``Detecting cusps and inflection points in curves.'' Comput. Aided Geom. Design 9, 1--24.


Accéder au sujet détaillé

Remarques:

The internship will take place at LIP6 at place Jussieu, in the center of Paris.

Interested candidates are encouraged to
contact me for additional information.


SL308-34 Contrôle d’un robot mobile par recherche arborescente Monte-Carlo  
Encadrement  
Encadrant : Olivier BUFFET(écrire)
Labo/Organisme : INRIA / LORIA
Ville : Nancy

Description  
Ce projet vise à aborder le problème du contrôle d'un système sous observabilité partielle (l'état n'étant qu'imparfaitement connu), formalisé dans le cadre des POMDP, et dans un monde continu. Plus concrétement, des approches à base d'algorithmes de recherche arborescente seront considérées pour contrôler un robot mobile simple.

Accéder au sujet détaillé

Remarques:
Le stage sera co-encadré avec Vincent Thomas (MCF à l'université de Lorraine).


SL308-35 Arrondis dirigés efficaces dans Coq  
Encadrement  
Encadrant : Érik MARTIN-DOREL(écrire)
Labo/Organisme : IRIT
Ville : Toulouse

Description  
Ce stage vise à évaluer la pertinence de l’implémentation en Coq d’approximations des arrondis dirigés en arithmétique à virgule flottante en se basant sur l’arrondi au plus proche. Les aspects à étudier comprennent bien entendu le temps d’exécution mais aussi la preuve formelle de ces implémentations.

Le développement formel pourra se baser sur la librairie Flocq formalisant l’arithmétique à virgule flottante en Coq.


Accéder au sujet détaillé

Remarques:
Co-encadrement avec Pierre Roux (pierre.roux@onera.fr)


SL308-36 Optimization of Spherical Harmonic Transforms and Rotations  
Encadrement  
Encadrant : Nathanaël SCHAEFFER(écrire)
Labo/Organisme : ISTerre / CNRS / Univ. Grenoble Alpes
Ville : Grenoble

Description  
The main goal is to improve (on CPU, C language) and/or implement (on GPU, cuda language) Spherical Harmonic related algorithms (transforms and rotations) targeting high performance computations.
You will learn the recently proposed algorithms, implement and/or optimize them and maybe even try to improve on them.
The resulting code should improve an existing open-source library.

Accéder au sujet détaillé


SL308-38 Mixed-representation state estimation  
Encadrement  
Encadrant : Francis COLAS(écrire)
Labo/Organisme : Loria
Ville : Nancy

Description  
Les robots autonomes ont besoin d'une représentation interne de leur environnement et de leur propre état.
Une technique très courante pour construire cette représentation est de recourir à des techniques d'estimation probabiliste comme les chaines de Markov ou le filtre de Kalman.
Ces techniques ont été appliquées avec succès à de nombreux problèmes de robotique en utilisant des représentations différentes des distributions de probabilité : discrétisation, échantillonnage, formes paramétriques...
Si l'on s'en tient à un type de représentation, les méthodes d'inférences sont relativement connues.
Le but de ce sujet est d'explorer l'inférence pour fusionner des distributions avec des représentations différentes.

Accéder au sujet détaillé


SL308-39 Formal verification of a messaging protocol  
Encadrement  
Encadrant : Véronique CORTIER(écrire)
Labo/Organisme : LORIA
Ville : Nancy

Description  
Context.
Security protocols are distributed programs that aim at ensuring security proper- ties, such as confidentiality, authentication or anonymity, by the means of cryptography. Such protocols are widely deployed, e.g., for electronic commerce on the Internet, in banking net- works, mobile phones and more recently electronic elections.
Formal methods have demonstrated their usefulness when designing and analyzing secu- rity protocols. They indeed provide rigorous frameworks and techniques that have allowed to discover new flaws. In particular, ProVerif [1] is a state-of-the-art tool dedicated to the security analysis of protocols. It takes as input the description of a protocol in the applied-pi calculus, a variat of the pi-calculus with a term algebra. It has been successfully applied to numerous protocols of the literature, providing security proofs or discovering new attacks.
While ProVerif has been successfully applied to complex large-scale protocols (e.g. TLS 1.3), there are still limitations when protocols have a complex datastructure and/or large- term shared memories. The goal of the internship is to evaluate the possibilities of ProVerif on a recent and challenging protocol : Asynchronous Ratcheting Trees (ART) [3], designed for asynchronous group messaging systems. It allows members to securely chat in groups while not being all online and support users to add and leave the group. Interestingly this protocol achieves post-compromise security : the key of a group remains secure even after compromission, provided that the attacker does not actively and continously interfere with the protocol.

Objectives of the internship.
The goal of the internship is to analyse the ART protocol in ProVerif. While this will start as a « standard » case study, we expect several challenges :
— the ART protocol relies on trees, for which ProVerif offers no support ;
— in the ART protocol, a new group key is built using previously generated keys, hence the protocol requires to model long-term states, for which ProVerif offers few support ;
— the property of post-compromise security is a new property that has never been for-
malised in ProVerif. This requires to define a new attacker model.
Therefore, the intern will need to develop sound (and clever ;-)) encodings to model such a protocol in the language of ProVerif. Alternatively, the intern may need to enhance ProVerif with new features, with the help of one of the developpers (Vincent Cheval). In particular, it should be possible to build upon recent developments of ProVerif, that include the treatment of stateful protocols and natural numbers [2].

One interesting aspect of the internship is that it mixes foundational work together with the study of practical protocols (messaging).


Accéder au sujet détaillé

Remarques:
co-encadrement avec Vincent Cheval.
Possibilité de rémunération.


SL308-40 Applications de l'algorithme de Sinkhorn à l’information quantique  
Encadrement  
Encadrant : Ion NECHITA(écrire)
Labo/Organisme : LPT Toulouse
Ville : Toulouse

Description  
Realiser une etude d’une généralisation non-commutative de l’algorithme de Sinkhorn. Au passage, apprendre les fondements de la théorie quantique de l’information.

Accéder au sujet détaillé


SL308-43 Traitement de géométrie en espace texture  
Encadrement  
Encadrant : David COEURJOLLY(écrire)
Labo/Organisme : LIRIS
Ville : Villeurbanne

Description  
Traitement de géométrie en espace texture
Objectifs du stage · Détails · Références
Objectifs du stage

En modélisation géométrique, une approche efficace pour la représentation d'objets complexes est de se baser sur une paramétrisation d'une géométrie simple à laquelle différentes modifications géométriques locales sont appliquées lors du rendu via des textures (normal map, displacement map...), en plus des textures liés à l'apparence de matière (couleur, roughness...).


Rapidement, la paramétrisation d'un objet associe, à chacun de ses triangles T, des coordonnées (u,v)∈[0,1)^2
à chacun de ses sommets. L'enjeu lorsque l'on calcule une telle paramétrisation est d'obtenir la transformation avec le moins de distorsion géométrique et le moins de découpes possible (e.g. une paramétrisation [0,1)2) de la sphère nécessite au moins une découpe). La littérature est large sur ce sujet, voir par exemple [Springborn08] [Soliman18]. Notez que lors de la production de contenu 3D, la surface n'est pas nécessairement simple topologiquement et plusieurs patchs de surfaces peuvent être utilisées sur un même espace de paramétrisation.

Récemment, une approche générique permet de reformuler certains opérateurs de traitement d'images (par exemple pour du débruitage) que l'on appliquerait sur les textures de manière à obtenir un résultat cohérent sur la surface [Prada18]. Intrinsèquement, ces opérateurs corrige la déformation métrique et opèrent de manière seamless au niveau des découpes. La généricité des opérateurs permet de résoudre des problèmes (variationnels) au-delà du simple traitement de l'image de texture comme de la propagation en distance :


Dans l'équipe, nous avons proposé quelques approches variationnelles permettant le traitement de géométrie en utilisant une formulation de Mulmford-Shah [Coeurjolly16] [Bonneel18]. Les objectifs du stage sont les suivants :

Reprendre les opérateurs génériques de [Prada18] dans les cas d'usages précisés par les auteurs (code disponible https://github.com/mkazhdan/TextureSignalProcessing ).
Utiliser ces opérateurs dans le contexte de la fonctionnelle de Mumford-Shah pour du débruitage lisse par morceaux dans l'espace des textures (cf [Bonneel18]).
Étendre ces outils pour le traitement des textures non-scalaires comme la normal map et la displacement map (cartes vectorielles plutôt que couleur par canal RGB).
Ce dernier point est clairement la partie la plus exploratoire du sujet. Cela permettrait d'avoir des outils de traitement de champs de vecteurs (tangents ou non) sur des surfaces uniquement sur la base de l'espace des textures sans distorsion ni discontinuité sur les découpes, et surtout sur des surfaces définies par une union de patchs.



Références

[Springborn08] Springborn, Boris, Peter Schröder, and Ulrich Pinkall. “Conformal equivalence of triangle meshes.” ACM Transactions on Graphics (TOG). Vol. 27. No. 3. ACM, 2008.
[Soliman18] Soliman, Yousuf, Dejan Slepčev, and Keenan Crane. “Optimal cone singularities for conformal flattening.” ACM Transactions on Graphics (TOG) 37.4 (2018): 105.
[Prada18] Prada, Fabián, et al. “Gradient-domain processing within a texture atlas.” ACM Transactions on Graphics (TOG) 37.4 (2018): 154.
[Bonneel18] Nicolas Bonneel, David Coeurjolly, Pierre Gueth, Jacques-Olivier Lachaud. Mumford-Shah Mesh Processing using the Ambrosio-Tortorelli Functional. Computer Graphics Forum (Proceedings of Pacific Graphics), 37(10), October 2018. https://perso.liris.cnrs.fr/david.coeurjolly/publications/bonneel18AT.html
[Coeurjolly16] David Coeurjolly, Marion Foare, Pierre Gueth, Jacques-Olivier Lachaud. Piecewise smooth reconstruction of normal vector field on digital data. Computer Graphics Forum (Proceedings of Pacific Graphics), 35(7), September 2016. https://perso.liris.cnrs.fr/david.coeurjolly/publications/coeurjolly16pg.html


Accéder au sujet détaillé

Remarques:
Le stage se déroulera au sein du laboratoire LIRIS (bat. Nautibus).

Encadrant : David Coeurjolly (LIRIS), Jacques-Olivier Lachaud (LAMA)

Compétences requises : C++, cmake, git, UEs d'image, d'analyse et de modélisation géométrique.



SL308-47 Automates cellulaires préservant un sous-shift  
Encadrement  
Encadrant : Samuel PETITE(écrire)
Labo/Organisme : LAMFA
Ville : Amiens

Description  
Pour un alphabet fini A, un sous-shift X ⊂ A^Z est un ensemble de suites qui est compact pour la topologie produit, et invariant par le shift (ou décalage). L’action du shift sur ces ensembles forment de riches familles de systèmes dynamiques chaotiques.
Le but de ce mémoire est d’étudier les automates cellulaires inversibles préservant un sous-shift donné. Ces automates forment alors une symétrie d’un point de dynamique, i.e. une auto-conjugaison (homéomorphisme de X commutant avec le shift). Cette étude est une question classique en système dynamique.

De récents résultats ont montré que les systèmes d’entropie nulle (complexité factorielle sous-exponentielle) présentent de fortes restrictions sur ces automates cellulaires. Une riche famille de tels sous-shifts est celle des sous- shifts Toeplitz connu pour donner de nombreux exemples et contre-exemples. Grâce à leurs propriétés arithmético-combinatoire, il est possible d’étudier leurs automorphismes de différents points de vue. Il en ressort que le groupe des automorphisme de ces systèmes est toujours abélien [2].
Ce mémoire est l’occasion d’appréhender les notions et les problématiques des systèmes dynamiques et de la théorie des groupes. Après avoir étudié un état de l’art via le livre [1] l’article [2] et ses références, en fonction de connaissance de l’étudiant, on tentera de réaliser la réciproque des résultats de [2], c’est-à-dire n’importe quel groupe dénombrable, avec des propriétés raisonnables, comme groupe d’automorphisme.

REFERENCES
[1] D. Lind and B. Marcus. An Introduction to Symbolic Dynamics and Coding. Cambridge University Press, 1995.

[2] S. Donoso, F. Durand, A. Maass, and S. Petite. On automorphism groups of Toeplitz sub- shifts, Discrete Analysis 2017:11, 19 pp.

Accéder au sujet détaillé


SL308-48 Formalisation des polyèdres dans l'assistant de preuve Coq  
Encadrement  
Encadrant : Xavier ALLAMIGEON(écrire)
Labo/Organisme : INRIA -- Ecole Polytechnique
Ville : Palaiseau

Description  
Les polyèdres convexes sont les ensembles de R^n définis par des systèmes d'inégalités linéaires (affines). Ils jouent un rôle majeur en mathématiques, et sont utilisés dans de nombreuses applications en informatique.

Le travail de stage s'inscrit dans le projet de formalisation de la théorie des polyèdres dans Coq, au sein de la bibliothèque Coq-Polyhedra. Deux exemples d'axes de travail sont proposés, en fonction des goûts du/de la stagiaire.

Le premier axe porte sur l'implémentation de l'élimination de Fourier--Motzkin dans la bibliothèque. Cet algorithme est une brique de base permettant de prouver facilement plusieurs propriétés clés sur les polyèdres. Son extraction vers du code exécutable présenterait un intérêt indépendant puisque l'algorithme est utilisé dans de nombreux solveurs SAT/SMT.

Le second axe porte sur la formalisation de techniques de preuve à base de perturbations dans Coq-Polyhedra. Il est en effet très fréquent dans les démonstrations sur les polyèdres de perturber certains objets par une petite quantité (typiquement un "epsilon"), de manière à exclure certaines configurations spéciales sans perte de généralité. Ce type d'arguments est particulièrement délicat à capturer dans un assistant de preuve, puisqu'il est nécessaire de quantifier explicitement l'ordre de grandeur de la perturbation à effectuer. On propose de manière alternative d'implémenter ces raisonnements en ayant recourt à des perturbations symboliques.

Accéder au sujet détaillé

Remarques:
Gratification possible


SL308-49 Accurate Prediction of Internet Threats Using Exogneous Data  
Encadrement  
Encadrant : Jérôme FRANÇOIS(écrire)
Labo/Organisme : Inria Nancy Grand Est
Ville : Nancy

Description  
-------
Context
-------

Predicting future cyber threats with reasonable lead-time and accuracy can give security practitioners sufficient time to prepare for upcoming major attacks. However, most prior work focuses on detecting attacks instead of predicting them. A notable exception is a recent paper [Zhenxin Zhan et al., 2015] by taking into account statistical temporal properties of cyber attacks. Unfortunately, that paper only achieves reasonable accuracy for a limited prediction time horizon (a few hours). Another notable exception [Liu et al., 2015] predicts security incidents on organizations by using security features about the organization such as network mismanagement symptoms. Unfortunately, that paper is unable to predict geo-politically motivated attacks. A promising direction to improve these prediction models is to take into account exogenous global social and technical data.

-------
Subject
-------

The goal of the internship is to model attack-related Internet traffic (from security sensors) to identify and predict large events or attack campaigns rather than looking into very fine-grained predictions. Hence, it is necessary to identify what is the proper level of granularity prediction techniques which can be considered as efficient, knowing that predicting next large campaigns to a particular region or country is already challenging. In particular, we will use a telescope and/or honeypot datasets that attract attacks at large scale and the question could be so briefly stated as follows “what can be accurately predicted from these data in the context of cybersecurity?”. Hence, different machine learning algorithms could be tested such as LTSM (Long short-term memory) networks in comparison with more regular approaches like ARIMA (Autoregressive integrated moving average)

While the analysis will focus first on Internet traffic, in particular packet- or flow-based information, the objective is also to include exogeneous data. For instance, some our honeypots gather credential tested by attackers that may reveal a strategy in targeted types of services or applications. Actually, it would be possible to infer some probing campaign strategies such as those supporting botnet construction. Generally, the second objective aims at linking discovered patterns in Internet traffic with external indicators giving context (honeypot, known data breaches…). Topic modelling techniques such as LDA (Latent Dirichlet Allocation) and vector representation of documents techniques such as doc2vec can be used to achieve this goal.

[Liu et al., 2015] Liu, Y., Sarabi, A., Zhang, J., Naghizadeh, P., Karir, M., Bailey, M., and Liu, M. (2015). Cloudy with a chance of breach: Forecasting cyber security incidents. In 24th USENIX Security Symposium (USENIX Security 15), pages 1009–1024, Washington, AZ.

[Zhenxin Zhan et al., 2015] Zhenxin Zhan, Maochao Xu, and Shouhuai Xu (2015). Predicting Cyber Attack Rates With Extreme Values. IEEE Transactions on Information Forensics and Security, 10(8):1666–1677.

Remarques:
Required skills
Good knowledge in Python programming, probabilistic and statistical methods, knwoledge in machine learning

Working environment
This internship takes place in LORIA/Inria Nancy Grand Est within the RESIST research team. The student will have access to data collected from available network security platforms hosted in the lab.


SL308-50 Few-shot learning for time series  
Encadrement  
Encadrant : Romain TAVENARD(écrire)
Labo/Organisme : IRISA - Obelix
Ville : Rennes

Description  
This internship will focus on the comparison of several embeddings for time series in terms of their applicability to few-shot learning settings.
Few-shot learning corresponds to learning problems in which very little supervised data is available for a given task.

A promising way to tackle this problems consist in relying on a meaningful embedding to compute attention scores between samples, as described in [3].
The proposition of such embeddings is hence of prime importance for the performance of these methods.
In this internship, we will focus on temporal data and consider two possible alternatives for such an embedding.
The first one is inspired by [2] in which an embedding is parametrized to mimic a target similarity measure called Dynamic Time Warping (DTW).
Another option would be to rely on the inherent temporal structure of the data at stake.
One could then train a Recurrent Neural Network (RNN) for a forecasting task [1] and use its hidden state as a time series embedding.

1] A. Graves. Generating sequences with recurrent neural networks. arXiv preprint arXiv:1308.0850, 2013.
[2] A. Lods, S. Malinowski, R. Tavenard, and L. Amsaleg. Learning dtw-preserving shapelets. In International Symposium on Intel ligent Data Analysis, pages 198–209. Springer, 2017.
[3] O. Vinyals, C. Blundell, T. Lillicrap, D. Wierstra, et al. Matching networks for one shot learning. In Advances in neural information processing systems, pages 3630–3638, 2016.

Accéder au sujet détaillé

Remarques:
Co-encadrement avec Simon Malinowski (IRISA - LinkMedia).
Possibilité de rémunération.


SL308-51 Neural-network-based clusterwise regression and classification  
Encadrement  
Encadrant : Simon MALINOWSKI(écrire)
Labo/Organisme : IRISA, Rennes, équipe LinkMedia
Ville : Rennes

Description  
Regression and classification are two well-know learning tasks. They aim at learning a regression function or a decision boundary from a training set of labeled examples.

Clusterwise methods aim at building different local models rather than one global model for a given learning task. This is particularly well adapted when different behaviors can be found in the data. Using such methods,complex decision boundaries or regression functions can be obtained using simple models.

Different techniques have been used to build clusterwise models. Some of them rely on first partitioning the data into clusters and then building local models inside each cluster, as in [1] for instance. Other techniques are based on the estimation of mixture models, as in [2].

In this internship, we are interested in building a framework for cluster-wise regression or classification based on neural networks (NN). The idea is to design a single NN model (global model) but composed of different sub-networks (that correspond to local models). The global model should be able to automatically learn the different local models of which it is composed. We hence aim at jointly learning a partition (soft or hard) and different local models.

The student will be in charge of :
1) Designing a clusterwise model based on Neural Networks
2) Apply this model to perform regression and classification on different kind of data
3) Assess the performance of this model compared to classical neural network models and other clusterwise methods.

The student will work with different kind of data, adapted for classifica-tion or regression.

[1] H. Späth. Clusterwise linear regression.Computing, 22(4) :367–373, Dec1979.

[2] C. Hennig. Identifiability of models for clusterwise linear regression.Jour-nal of Classification, 17(2) :273–296, Jul 2000

Remarques:
Co-encadrement avec Romain Tavenard
Possibilité de rémunération



SL308-52 SImulation hybride différentielle-stochastique  
Encadrement  
Encadrant : François FAGES(écrire)
Labo/Organisme : Inria Saclay
Ville : Palaiseau

Description  
Le formalisme des réseaux de réactions chimiques (CRN) est utilisé pour modéliser les processus biologiques au niveau cellulaire. Ils expliquent les phénotypes complexes comme résultant d'interactions moléculaires élémentaires. Un CRN a une structure d'hypergraphe (c'est-à-dire graphe biparti espèce / réaction étiquetée par une fonction de taux) et peut être interprété à différents niveaux d'abstraction dans une hiérarchie de différentes dynamiques: différentielle, stochastique, discrète réseau de Petri ou booléenne. Les simulations différentielles et stochastiques peuvent permettre des prévisions quantitatives, tandis que les interprétations réseau de Petri et booléenne peuvent servir à des fins d'analyse à un niveau d'abstraction élevé, sans information sur la cinétique des réactions.

L'algorithme de simulation stochastique (SSA) fournit une intégration numérique de l'équation maitresse chimique (chaine de Markov à temps continu). L'équation différentielle ordinaire associée à un CRN est une approximation au premier ordre du comportement stochastique moyen, qui est beaucoup plus efficace à calculer par intégration numérique (en utilisant des méthodes implicites pour des systèmes raides) que par simulation stochastique, mais qui n'est pas correcte pour les petits nombres de molécules.

Les simulations hybrides stochastiques-différentielles visent à fournir des stratégies dynamiques automatiques permettant de combiner les deux algorithmes de simulation avec des critères généraux assurant à la fois l'exactitude et une efficacité maximale.

Le travail pratique de ce stage consiste à mettre en œuvre (dans Prolog) dans BIOCHAM-4 la stratégie dynamique décrite dans le présent document, en utilisant à la fois l'intégrateur différentiel et le mécanisme d'événement comme moyen de mise en œuvre de la SSA.

La recherche consistera à expérimenter plus avant les stratégies de partitionnement dynamique décrites dans le document et à les évaluer sur le référentiel de modèles BioModels.

Des travaux théoriques sur ce sujet sont possibles concernant la preuve des critères de correction, ainsi que par exemple la recherche de critères plus faibles que l’approximation à tous points de temps.

Remarques:
co-encadrement Sylvain Soliman

Gratification 530euros mensuel


SL308-53 Visualisation de réseaux de réactions biochimiques utilisant des analyseurs statiques  
Encadrement  
Encadrant : François FAGES(écrire)
Labo/Organisme : Inria Saclay
Ville : Palaiseau

Description  
Le formalisme des réseaux de réactions chimiques (CRN) est utilisé pour modéliser les processus biologiques au niveau cellulaire. Ils expliquent les phénotypes complexes comme résultant d'interactions moléculaires élémentaires. Un CRN a une structure d'hypergraphe (c'est-à-dire graphe biparti espèce / réaction étiquetée par une fonction de taux) et peut être interprété à différents niveaux d'abstraction avec différentes dynamiques: différentielle, stochastique, discrète réseau de Petri ou booléenne.

La visualisation de la structure des CRNs n'est pas un problème bien résolu aujourd'hui, et les outils de dessin automatique sont très loins de pouvoir rivaliser avec les dessins manuels que réalisent les modélisateurs dans les publications, et qui montrent beaucoup mieux la "logique" du réseau.

Avant d'effectuer des simulations, nombre d'analyseurs statiques permettent cependant de fournir des informations sur les entrées et sorties du réseau, graphe de dépendance et influences, ainsi que sur les propriétés dynamiques, comme par exemple les invariants algébriques ou place-invariants du réseau de Petri (ensemble d'espèces moléculaires dont la somme des concentrations est constante), transition-invariants (ensemble de réactions formant un circuit), etc.

Le but du stage est de chercher à utiliser ces informations statiques (calculées par BIOCHAM) sur la structure du réseau de façon à définir des stratégies de dessin et à paramétrer les outils de visualisation du graphe d'interaction ( Graphviz) de telle sorte qu'il produise des dessins automatiques se rapprochant des dessins manuels que l'on trouve dans les publications.

Accéder au sujet détaillé

Remarques:
co-encadrant sylvain soliman

gratification 530 euro mensuel


SL308-54 SATisfaisabilité booléenne modulo Equations Différentielles pour vérifier les réseaux de réactions chimiques  
Encadrement  
Encadrant : François FAGES(écrire)
Labo/Organisme : Inria Saclay
Ville : Palaiseau

Description  
Les solveurs de contraintes booléennes SAT ont montré des performances remarquables pour la preuve de circuits et de programmes. Le besoin de raisonner sur des structures de données plus riches que les booléens a conduit à les généraliser à des solveurs SAT modulo Théories, en combinant les techniques de résolution SAT à d'autres techniques de résolution de contraintes arithmétiques ou autres, telles que: programmation linéaire, arithmétique d'intervalles, programmation par contraintes.

En particulier, les solveurs SAT modulo équations différentielles, permettent de raisonner sur la dynamique continue d'un système solution d'équations différentielles lorsque les valeurs de paramètres ou les valeurs initiales ne sont pas connues précisémment mais sont données dans un intervalle de valeurs.

Les travaux fondateurs de 2008 ont conduit à des implémentations (ex. système dReal) qui ont permis de prouver des propriétés d'accessibilité dans les systèmes hybrides paramétrés.

Ces résultats sont particulièrement intéressants dans les contextes de la biologie calculatoire des systèmes ou de la biologie synthétique, car dans ces systèmes les paramètres des systèmes de réactions biochimiques ne sont pas connus précisément et sujets à de fortes variations. Le sujet du stage est d'évaluer ces techniques dans ce contexte comparativement aux techniques de model-checking bornée implémentées dans BIOCHAM.

Le stagiaire aura pour mission d'essayer les systèmes SAT modulo ODE existants, et de les évaluer sur les exemples de systèmes biologiques que nous traitons dans l'équipe avec BIOCHAM.

Accéder au sujet détaillé

Remarques:
co-encadrement Sylvain Soliman

gratification 530 euros mensuel


SL308-55 Analyse des déplacements du spectrographe ELT/HARMONI à partir d’observations astrophysiques  
Encadrement  
Encadrant : Johan RICHARD(écrire)
Labo/Organisme : CRAL
Ville : Saint-Genis-Laval

Description  
Le CRAL est un laboratoire de recherche en astrophysique (UMR CNRS/Université Claude Bernard Lyon1/ENSL), qui regroupe environ 90 personnes (chercheurs, étudiants, ingénieurs, techniciens et administratifs). Il est un acteur majeur de l’instrumentation pour les grands observatoires astronomiques. Il est aujourd’hui engagé dans la réalisation d’instruments dans le cadre de très grands projets internationaux, en particulier HARMONI, qui est l’un des 2 premiers instruments qui équipera l’Extremely Large Telescope (ELT) à l’horizon 2024. Le CRAL a entre autres la responsabilité de développer les logiciels de simulation et de réduction des données de l’instrument.

Résumé du travail demandé :
HARMONI est un spectrographe intégral de champ : il découpe la zone du ciel observée en un grand nombre de points afin d’en obtenir simultanément les spectres lumineux, qui sont enregistrés par des détecteurs. Le logiciel de réduction des données transforme les images des détecteurs en un cube de données en s’appuyant sur des images d’étalonnage qui permettront de déterminer avec précision la transformation entre les données détecteur et le cube de données. Cependant des déplacements opto-mécaniques dans l’instrument pendant le laps de temps qui sépare les observations sur le ciel des images d’étalonnage peuvent rendre ces dernières inutilisables sans analyse plus poussée.

Le but du stage sera d’explorer, et éventuellement développer, un ensemble de méthodes qui permettront de quantifier ces déplacements en analysant les images faites sur le ciel. Les méthodes classiques telles que la recherche de patterns ou la détection des bords de spectre semblent mal adaptées dans les cas à faible rapport signal sur bruit. Les méthodes identifiées devront couvrir les 44 configurations de l’instrument, ainsi que la grande diversité des observations sur le ciel. Elles devront également évaluer la précision de la mesure retournée afin de déterminer la méthode optimale pour chaque cas. L’étudiant(e) pourra prototyper cet ensemble de méthodes en Python en les testant et les validant sur des images simulées de l’instrument HARMONI et sur des images obtenues avec des instruments similaires (MUSE, KMOS).

Compétences :
• Méthodes numériques et calcul scientifique (traitement d’image, traitement du signal, algèbre linéaire, etc.).
• Langage Python, système d’exploitation Linux.
• Lecture de documentations techniques en anglais (aptitude à la rédaction du rapport technique en anglais souhaitable).



Accéder au sujet détaillé

Remarques:
Co-encadrement par Aurélien Jarno de l'équipe informatique scientifique.

Gratifications : environ 500€ par mois, selon le barème défini dans le code de l’éducation.


SL308-56 Caractérisation de traces de navigation  
Encadrement  
Encadrant : Lionel TABOURIER(écrire)
Labo/Organisme : LIP6 (Sorbonne Université / CNRS)
Ville : Paris

Description  
voir description complète dans fichier pdf

Accéder au sujet détaillé

Remarques:
Le stage est co-encadré par Pedro Ramaciotti (LIP6) et Christophe Prieur (Télécom Paris Tech)


SL308-57 Modèle de dimères sur les groupes de Baumslag-Solitar  
Encadrement  
Encadrant : Nathalie AUBRUN(écrire)
Labo/Organisme : LIP - UMR 5668
Ville : Lyon

Description  
Combien y a-t-il de façon de paver un échiquier de forme rectangle $m\times n$ avec des dominos ? La réponse à cette question en apparence simple a été donnée par Kasteleyn (1961) et Temperley et Fisher (1961) en utilisant des méthodes différentes. De cette formule on déduit une formule asympotique pour le modèle des dimères, où l'on dispose des dominos sur une grille infinie, qui nous donne notamment l'entropie de ce modèle.

Le modèle des dimères est à la croisée de plusieurs domaines : combinatoire, physique statistique, dynamique symbolique. Il est plutôt bien compris lorsque l'on dispose des dominos sur une grille de taille infinie (que l'on peut voir comme le graphe de Cayley du groupe Z^2 avec sa présentation usuelle <a,b l ab=ba>). On peut définir un modèle des dimères sur n'importe quel graphe infini biparti, et chercher à calculer son entropie, comprendre la structure des ensembles de pavages possibles d'un sous-graphe fini. Pour l'entropie, des résultats sont connus essentiellement dans le cas de graphes planaires, ou lorsque le graphe ne contient pas le graphe biparti complet K_{3,3} comme mineur : on peut notamment calculer le nombre de pavages possibles d'un sous-graphe fini fixé en temps polynomial (Lovasz & Plummer, 2009).

Le but du stage sera de s'intéresser au modèle des dimères sur un graphe biparti qui contient K_{3,3} comme mineur, le graphe de Cayley du groupe de Baumslag-Solitar BS(1,3). Ce groupe a pour présentation BS(1,3):=< a,b l ab=ba^3>.
Ce groupe est moyennable, ce qui permet de définir l'entropie du modèle des dimères de manière similaire à ce qui est fait dans la grille infinie Z^2.

Objectifs du stage :

- Comprendre le modèle des dimères sur Z^2.
- Comprendre le groupe BS(1,3) et son graphe de Cayley.
- Définir une opération de flip et une fonction hauteur pour montrer la flip-connexité de l'ensemble des pavages d'un sous-graphe fini fixé ;
- Calculer la fonction de complexité et l'entropie du modèle (formule close et/ou approximation).

Accéder au sujet détaillé

Remarques:
Ce stage sera co-encadré par Etienne Moutot.

Possibilité de rémunération.


SL308-59 ProvenMPFR  
Encadrement  
Encadrant : Paul ZIMMERMANN(écrire)
Labo/Organisme : Inria Nancy-Grand Est / LORIA
Ville : Nancy

Description  
voir lien vers pdf

Accéder au sujet détaillé

Remarques:
collaboration avec Karthik Bhargavan, équipe Prosecco, Inria Paris


SL308-60 Formal proofs in Coq for visibility walks  
Encadrement  
Encadrant : Yves BERTOT(écrire)
Labo/Organisme : Inria
Ville : Sophia Antipolis

Description  
The goal of this internship is to verify an algorithm from computational geometry: the visibility walk algorithm. This algorithm is used to find the triangle containing a given point inside a triangulation.

Most of the work will consist in programming in the purely functional programming language of the Coq system, using simple inductive data-types and data-types taken from the Mathematical Components library. Then the intern will develop proofs of correctness for the algorithm, mostly using the ssreflect variant of the Coq system and the theorems from the Mathematical Components library.

In the long run, we hope this work to have applications in robotics, for instance in motion planning.

Accéder au sujet détaillé


SL308-62 Model-checking pour logiques temporelles d'intervalles  
Encadrement  
Encadrant : Stéphane DEMRI(écrire)
Labo/Organisme : LSV
Ville : Cachan

Description  
Les logiques temporelles utilisées dans l'approche par model-checking pour la vérification
possèdent des modèles dont l'unité de base est l'instant alors que dans les logiques temporelles
d'intervalles, c'est l'intervalle qui est l'élément atomique des modèles. Dans ces logiques d'intervalles,
les modalités permettent d'exprimer des contraintes sur les intervalles (les fameuses
relations de Allen). Alors que le problème de satisfiabilité pour des fragments
de logiques d'intervalles a été très étudié, le problème de model-checking n'a été introduit
et étudié que beaucoup plus récemment. Sous hypothèse de condition d'homogénéité (un intervalle
composé d'une séquence d'états satisfait une variable propositionnelle ssi tous les
états de la séquence satisfait la variable), le problème de model-checking pour la logique d'intervalles de
Halpern et Shoham est montré décidable en utilisant la technique des BE-descripteurs.
Dans un travail suivant, la condition d'homogénéité est généralisée
et une procédure de décision non-élémentaire est conçue, mais cette fois à base d'automates finis.


Le premier objectif de ce stage consiste à se familiariser avec les logiques temporelles d'intervalles
en relation avec les problèmes de satisfiabilité et de model-checking. Dans un second temps, on
étudiera les deux preuves qui permettent de montrer que le model-checking de la logique d'intervalles
de Halpern et Shoham sous la condition d'homogénéité est décidable mais avec
une procédure de décision de complexité non-élémentaire.
Une comparaison des deux méthodes est attendue, et cela dans le but d'essayer d'améliorer
la complexité. Comme la meilleure borne inférieure
de complexité pour ce problème est EXPSPACE, si le temps le permet, on pourra
s'attaquer à réduire le fossé entre EXPSPACE et la non-élémentarité.

Accéder au sujet détaillé


SL308-64 Bounded model checker for threshold automata with delays  
Encadrement  
Encadrant : Igor KONNOV(écrire)
Labo/Organisme : INRIA Nancy Grand Est
Ville : Nancy

Description  
Context. The internship topic concerns the parameterized verification of fault-tolerant distributed algorithms such as distributed consensus, agreement, and fault-tolerant clock synchronization. In such algorithms, the participants communicate by exchanging messages, in order to arrive at a common decision. The problem is aggravated by the presence of faults: some participants may crash and some may exhibit Byzantine behaviors such as lie about their state. As fault-tolerant algorithms are notoriously difficult to design right, one needs verification tools that check whether a fault-tolerant distributed algorithm is indeed robust to faults.

Objectives. The authors of [1, 2] modelled fault-tolerant distributed algorithms with threshold automata. They have shown that one can verify safety of parameterized systems of threshold automata by constructing queries to an SMT solver. This result was achieved under the assumption of asynchronous reliable communication, that is, every message is guaranteed to be delivered, although there is no upper bound on the delivery time. This model is known to be too permissive: It is impossible to solve consensus under the assumptions of pure asynchrony [3]. To circumvent this problem, many fault-tolerant distributed algorithms work under timing assumptions: every message is delivered in a time interval [min_delta, max_delta], where min_delta and max_delta are predefined constants. One can model such algorithms by using threshold automata with delays.

Recently, it was found that accelerated systems of threshold automata with time constraints have bounded diameters [4], similar to the accelerated systems of ordinary (non-timed) threshold automata. Hence, in this internship work, we propose to extend the verification approach of [2] to threshold automata with delays. This work requires: (1) fundamental contributions on how to extend the SMT schemas to schemas with delays, (2) an extension of the existing Byzantine model checker to support verification of threshold automata with delays.


Accéder au sujet détaillé


SL308-65 Bounded model checking of liveness properties of TLA+ specifications  
Encadrement  
Encadrant : Igor KONNOV(écrire)
Labo/Organisme : INRIA Nancy Grand Est
Ville : Nancy

Description  
Context. TLA+ [1] is a language that was designed for the formal specification of systems such as concurrent and distributed algorithms. It is currently supported by the explicit-state model checker TLC and the interactive TLA+ Proof System TLAPS. In the ongoing project APALACHE [2,3], we are developing a symbolic model checker for TLA+ as a complement to TLC, which relies on state enumeration. In contrast, the bounded model checker generates constraints describing counter-examples to claimed properties that are then discharged by an SMT solver.

Objectives. The overall procedure of symbolic model checking works as follows: (1) it identifies symbolic transitions in a TLA+ specification [4], and (2) it encodes bounded executions and safety properties as constraints in the input language of the SMT solver. The current version verifies whether a bounded execution reaches a state that violates a system invariant provided by the user. These properties belong to the class of safety properties: The system is doing nothing "bad".

It is well understood that safety property alone does not guarantee that a system is doing anything useful. In order to prove that the system is going to achieve a "good" state, one has to prove liveness of the system. For instance, one might want to prove that the system eventually reaches a state in which all the system components have finished their computations. In this work, we propose to extend the APALACHE model checker with techniques for bounded model checking of temporal properties. The intern is expected to implement the well-known technique by Biere et. al. [5] in the model checker for TLA+, which currently supports only finite-state systems. If successful, an extension with the technique recently suggested by Padon et. al. [6] can be envisaged, which, in principle, applies to infinite-state systems.

Accéder au sujet détaillé


SL308-67 Temporal Data Mining: Learning from Positive Examples  
Encadrement  
Encadrant : Nicolas BASSET(écrire)
Labo/Organisme : Verimag/UGA et CNRS
Ville : Saint-Martin D'Heres

Description  
Le stage se propose d’étudier l'apprentissage formel de fonctions booléennes et/ou d'automates a partir d'un ensemble de séquences de vecteurs booléens donnes. Ces séquences modélisent par exemple un échantillon de comportements de systèmes cyber-physiques (tels que ceux utilisés par nos collaborateurs de Toyota).
Le problème consiste a trouver un ensemble/langage a la fois succinct et simple qui contiennent (et rendent bien compte de) l’échantillon de séquences donnés a l'entrée de l'algorithme. Plusieurs variantes du problème peuvent être définies, suivant par exemple que l’échantillon soit fixe ou dynamique.
La définition des problèmes considérés est aisément accessible avec des connaissances de bases de logique booléennes et de théorie des langages.
Les objectifs poursuivis par l’étudiant sont selon son inclination:
-trouver des algorithmes et heuristiques efficaces pour les problèmes d’apprentissage définies
-guider sa recherche en menant des expériences en utilisant le langage de programmation de son choix (C, Python, OCAML,...)
-démontrer des résultats théoriques tels que des bornes de complexités pour les problèmes considérés (par exemple tel problème est NP dure mais dans PSPACE...)


Accéder au sujet détaillé

Remarques:
Co-encadrement par Thao Dang,
Rénumération possible.


SL308-68 Characterizing the Performance Limits of the PLC G3 (Linky)  
Encadrement  
Encadrant : Nicolas GAST(écrire)
Labo/Organisme : LIG / Inria
Ville : Grenoble

Description  
Enedis is currently deploying 35 millions of smart meters (called Linky). They use PLC to communicate.

The main objective on the internship will be to contribute to the understanding of the limits of the PLC G3 protocol. To do so, the intern will:
- construct and study a stochastic model of the MAC layer of the CPL G3 implemented in the Linky.
- use approximation techniques to characterize the performance bottleneck
- implement a stochastic simulator in order to compare the obtained models and real traces that have already been collected.

Accéder au sujet détaillé

Remarques:
Possibilité de rémunération, co-encadrement avec Mouhcine Mendil (post-doctorant).


SL308-69 Secure compilation of side-channel countermeasures  
Encadrement  
Encadrant : Deepak GARG(écrire)
Labo/Organisme : MPI for Software Systems
Ville : Saarbrucken

Description  
Many security-critical implementations are vulnerable to side-channel attacks, where an attacker uses physical observations about program execution (time, energy consumption) to retrieve confidential data, for instance cryptographic keys. Software-based countermeasures and
policies could provide an effective protection against side-channel attacks. Unfortunately, applying countermeasures and policies on source programs is problematic, because compilers generally do not preserve security.

The internship will study interactions between compiler optimizations and software-based countermeasures. The concrete objective will be to prove preservation of selected software-based countermeasures, using an adaptation of a recently proposed technique for cache-based timing
channels [1]. The work will initially focus on the class of constant resource programs, i.e. whose ressource consumption is independent of secrets [2]. Other countermeasures and policies will be considered if
time allows.

[1] Gilles Barthe, Benjamin Grégoire, Vincent Laporte: Secure
Compilation of Side-Channel Countermeasures: The Case of Cryptographic
"Constant-Time". IEEE Symposium on Computer Security Foundations 2018:
328-343

[2] Van Chan Ngo, Mario Dehesa-Azuara, Matthew Fredrikson, Jan
Hoffmann: Verifying and Synthesizing Constant-Resource Implementations
with Types. IEEE Symposium on Security and Privacy 2017: 710-728



Remarques:

The internship will be co-supervised by Deepak Garg (MPI for Software Systems) and Gilles Barthe (MPI for Security and Privacy). Students will receive a stipend.


SL308-70 Validation incrémentale de schémas pour graphes RDF  
Encadrement  
Encadrant : Iovka BONEVA(écrire)
Labo/Organisme : équipe Links de Inria Lille
Ville : Villeneuve d'Ascq

Description  
Le RDF est le format de données graphe utilisé dans le Web des données ou dans les bases de connaissances. Il est possible de décrire et vérifier des schémas (ou contraintes) pour des données RDF en utilisant des langages dédiés, tels Shape Expression Schemas ou SHACL. Cependant, même une petite modification dans le graphe peut entraîner la violation de plusieurs contraintes liées au schémas.

Lors du stage, l'étudiant.e devra identifier de quelle manière les modifications du graphe peuvent impacter sa validité par rapport à un schéma, et proposer un algorithme de validation incrémentale. L'algorithme permettra de vérifier si le schéma est toujours valide après modification du graphe, en évitant de visiter la totalité du graphe.


Accéder au sujet détaillé

Remarques:
Aide pour payer le logement de l'étudiant.e sur place. Me contacter pour plus de renseignements.


SL308-71 Proof systems based on restricted Boolean circuits  
Encadrement  
Encadrant : Florent CAPELLI(écrire)
Labo/Organisme : CRIStAL, Université de Lille
Ville : Lille

Description  
In this internship, we propose to look at proof systems based on syntactically restricted circuits. We are mainly interested in designing proof systems for \#SAT, the problem of counting the number of satisfying assignments of a CNF formula, that is, we want to design a system such that if we are given a CNF formula $F$ with $k$ satisfying assignments, one can write a proof $P$ that can be checked in polynomial time in the size of $P$ that $F$ has indeed $k$ satisfying assignments. We propose to use restricted Boolean circuits arising in the field of Knowledge Compilation as proofs so that $P$ is such a restricted circuit representing all solutions of $F$ and so that one can both check that $P$ represents $F$ and count the number of satisfying assignments of $P$ in polynomial time in the size of the circuit.

Accéder au sujet détaillé


SL308-72 Traitement audio très faible latence sur FPGA par synthèse de haut niveau  
Encadrement  
Encadrant : Florent DE DINECHIN(écrire)
Labo/Organisme : CITI, INSA Lyon
Ville : Lyon

Description  
Faust (Functional Audio Stream, https://faust.grame.fr), développé par le GRAME à Lyon, est un langage de programmation spécifiquement conçu pour les applications de traitement du signal en temps réel pour l’audio.
Le compilateur Faust permet de développer rapidement des logiciels efficaces et fiables pour les principales plateformes audios (plugins VST et AU, Max/MSP, PureData, applications macOS, iOS, Android, Web, Linux, etc.).
Faust connaît depuis quelques années un grand succès autant dans la communauté de recherche en informatique musicale, qu’au niveau des développeurs professionnels (Moforte, Analog Devices) ou du grand public (ex : http://www.grame.fr/prod/geek-bagatelles).

Une limitation de ces applications est la latence: le traitement logiciel du son implique que chaque buffer audio traverse plusieurs couches logicielles entre la carte son et le système d’exploitation, impliquant un délai de quelques millisecondes pour tout traitement sonore.
Mais certaines applications, telles que la correction active de la résonance d’un instrument acoustique, nécessitent des latences de l’ordre de un ou deux échantillons (moins de 50 microsecondes).
Une solution à ce problème serait de compiler Faust vers un pipeline de traitement du signal implémenté dans un un circuit reconfigurable (FPGA). C'est l'objectif de ce stage.

La programmation des FPGAs est beaucoup plus complexe que celle des ordinateurs classiques.
Ce stage s'appuiera sur l'expertise du CITI en traitement du signal sur les FPGA, en particulier autour du générateur de VHDL FloPoCo (\url{http://flopoco.gforge.inria.fr/}).

Une des difficulté de ce projet sera la prise en main d'une carte FPGA, la carte Digilent Zybo-Z7.
Elle intègre une puce audio capable d'échantillonage comme de synthèse sonore, et une puce Xilinx intégrant du circuit reconfigurable et des coeurs ARM sous Linux.
Un premier challenge technique sera de modifier la configuration par défaut de cette carte pour que l'audio puisse être traitée directement par la partie FPGA sans passer par le software d'exécutant sur Linux.
Le matériel comme le logiciel sont ouverts, et plusieurs projets github peuvent servir de point de départ.
Le second challenge sera de compiler Faust vers du matériel. On pourra commencer en utilisant VivadoHLS, le compilateur C vers matériel de Xilinx. L'objectif est de réaliser un démonstrateur de traitement sonore à très faible latence.

Le candidat sera basé à Lyon, dans l'équipe Socrate du CITI sur le campus de la Doua.
Il se fera en collaboration forte avec l'équipe des chercheurs de GRAME responsable du développement de Faust.

La maîtrise du langage C ainsi que des bases solides en architecture des ordinateurs sont indispensables.
Il est souhaitable que le stagiaire s'intéresse aussi à la compilation, à la programmation système, à la programmation des FPGAs, ou (inclusif) à la musique.

Remarques:
Ce stage s'inscrit dans le projet SyFaLa entre GRAME et le CITI, et une gratification est possible.
Côté GRAME (Faust), ce travail sera suivi par Yann Orlarey, développeur de Faust. Côté CITI, il sera encadré par Florent de Dinechin et Tanguy Risset.


SL308-74 Analyse de motifs dans des graphes de paiement entre entreprises  
Encadrement  
Encadrant : Nazim FATÈS(écrire)
Labo/Organisme : INRIA Nancy - LORIA
Ville : Nancy

Description  
Une grande partie des modèles macroéconomiques repose sur des données agrégées, c'est-à-dire sur des moyennes ou des distributions des différents paramètres qui règlent le comportement des acteurs. Cette agrégation cependant dissimule la réelle structure des rapport d’échange et payement qui lient entre eux les acteurs économiques dans leurs interactions effectives. Le but de ce stage est d'analyser la structure d'un ou plusieurs graphes qui modélisent les rapports de paiement entre entreprises. Nous cherchons à identifier des motifs intéressants de tels graphes afin de comprendre ce que peut apporter une vue réelle et décentralisée des échanges économiques. Nous cherchons en premier lieu à identifier la présence de cycles : si une première entreprise émet une facture pour une seconde entreprise, laquelle émet une facture pour une autre et ainsi de suite, jusqu'à ce que la chaîne se referme sur elle-même, on est alors en présence d'un cycle potentiellement vertueux, qui peut faciliter les échanges car chaque acteur sait que s'il paye sans tarder, il sera payé à son tour. Ainsi une compensation entre les acteurs s’installe réduisant le besoin total de liquidités. De même, nous serons intéressés par l'identification des chaînes longues dans lesquelles de nombreux acteurs peuvent annuler leurs dettes réciproques, pourvu que le premier acteur soit financé par le même intermédiaire que le dernier acteur remboursera. Enfin, nous chercherons à développer les moyens de visualiser la forme de ces graphes de paiement et d'en identifier les qualités de robustesse ou de faiblesse.

Le travail s'effectuera sur des données réelles et sur des modèles simulés. Il se fera en priorité en java. Il comportera une partie d'"invention" d'heuristiques de recherche, lesquelles pourront utiliser des systèmes dynamiques discrets décentralisés (automates cellulaires déterministes ou probabilistes, systèmes multi-agents, etc.).



Remarques:
Ce stage pourra se dérouler en dialogue avec Massimo Amato (université de Bocconi de Milan) pour la partie économie et Irène Marcovici (université de Lorraine) pour la partie graphes et systèmes dynamiques.


SL308-75 Les espaces cohérents comme modèle du 𝜆-calcul polymorphe  
Encadrement  
Encadrant : Thomas SEILLER(écrire)
Labo/Organisme : LIPN -- UMR 7030
Ville : Villetaneuse

Description  
La sémantique dénotationelle est une branche de la théorie des langages de programmation. Elle cherche à modéliser des programmes écrits dans des langages abstraits – tel le 𝜆-calcul, qui a servi de modèle à la programmation fonctionnelle – par des objets mathématiques structurés. On espère ainsi qu’une étude de ces modèles au moyen d’outils mathématiques poussés nous éclaire sur les propriétés des langages concernés.

Le langage qui nous intéresse ici est le 𝜆-calcul polymorphe (appelé aussi système F) qui est à la base des langages fonctionnels typés tels que OCaml ou Haskell. Un modèle de ce langage, basé sur des graphes nommés espaces cohérents, a été proposé par Jean-Yves Girard au milieu des années 1980.

Cependant, aucune preuve complète du fait que les espaces cohérents modélisent correctement le 𝜆-calcul polymorphe n’existe dans la littérature. Il est d’ailleurs connu que l’article original de Girard comporte un « bug » significatif, dont un correctif fait partie du folklore. Un problème lié est que les espaces cohérents n’ont jamais été rattachés formellement à une définition axiomatique des modèles du 𝜆-calcul polymorphe, telle que la notion de PL-catégorie issue de la théorie des catégories.

Le but du stage est de définir la PL-catégorie des espaces cohérents, et d’établir rigoureusement qu’elle vérifie bien les axiomes des PL-catégories.

Accéder au sujet détaillé

Remarques:
Co-encadrant: Lê Thành Dũng Nguyễn (lethanhdung.nguyen@lipn.fr).


SL308-76 Paramétricité pour les langages avec effets  
Encadrement  
Encadrant : Guillaume MUNCH-MACCAGNONI(écrire)
Labo/Organisme : Equipe Gallinette, Inria
Ville : Nantes

Description  
Il s'agit d'un sujet pour les étudiants avec un goût prononcé pour les mathématiques, qui ont aimé le cours de PROG et/ou dont le séminaire de théorie des catégories ou la correspondance de Curry-Howard ont suscité la curiosité.

Un joli post de blog, [http://prl.ccs.neu.edu/blog/2017/06/05/syntactic-parametricity-strikes-again/], attirait notre attention sur le fait, semble-t-il peu connu, que les techniques de recherche de preuve permettent d'obtenir très facilement des théorèmes de paramétricité. C'est lié à une technique simple et élégante expliquée dans Girard et al. (1992) qui mériterait effectivement d'être mieux connue et expliquée aux gens qui s'intéressent à la théorie des langages de programmation (qui bien souvent on des effets de bord: non-terminaison, opérateurs de contrôle, état, exceptions...).

La paramétricité est à la base de l'interprétation calculatoire du système F (le λ-calcul polymorphe). Par exemple, pour tous termes clos t,u du système F de types respectifs ∀α((A→α)→α) et A→B, l'analyse des formes normales donne: u(t(λy.y))=tu. Cela implique, dans les modèles intéressants de système F, l'isomorphisme ∀α((A→α)→α)≅A, à la base de l'interprétation des type de données dans le système F, par exemple ∀α((A→α)→(B→α)→α)≅∀α(((A+B)→α)→α)≅A+B: autrement dit, le type des booléens de Church est bien un type booléen! et autres propriétés du genre.

L'idée de Girard et al. (1992) est très simple: on montre que la propriété est vraie pour les formes normales, puis on montre que les termes normalisent. On montre en fait un résultat de paramétricité pour tous les jugements de types simples F(α)⊢G(α) à la fois, en énonçant avec le langage de la théorie des catégories que ce sont des transformations dinaturelles (ci-dessus, exemple avec F(α)=A→α et G(α)=α). Les transformations dinaturelles forment presque un modèle, il leur manque juste la composition! C'est là que la normalisation (= élimination de la composition) intervient. Cela établit en réalité un lien fondamental entre 1) paramétricité dans les langages de programmation, 2) élimination des coupures en théorie de la démonstration, et 3) théorèmes de cohérence en théorie des catégories.

Toute la partie de théorie de la démonstration peut être reformulée de façon moderne, auto-suffisante, concise et rigoureuse grâce à des techniques récentes (Munch-Maccagnoni, 2017, Thms 55, 56, 66, 67). Mais il y a mieux! En faisant cela, on se rend compte qu'on n'utilise pas toutes les équations du langage d'origine. Le travail pré-cité caractérise les équations dont on a besoin, en les rapprochant des modèles du λ-calcul avec effets de bord, qui forcent un ordre d'évaluation (un modèle standard appelé le call-by-push-value, CBPV). Par conséquent, cela mène a généraliser le résultat de paramétricité de Girard et al. (1992) aux langages avec effets. Toute la difficulté est de savoir comment étendre l'énoncé du résultat dans ce nouveau cadre. Cela devrait se passer comme dans Levy (2017) qu'on pourra retrouver comme un cas particulier. On peut également s'en inspirer pour réfléchir à l'implication du résultat pour des cas d'effets concrets (non-terminaison, etc.).

Le stage est en deux étapes. La première étape est bibliographique et consiste à comprendre ce que j'ai raconté ci-dessus. Le résultat sera une reformulation concise et avec des techniques modernes du résultat de Girard et al. (1992). La deuxième consiste en une généralisation aux modèles avec effets de bord. Le but est d'obtenir un résultat qui généralise à la fois Girard et al. (1992) et Levy (2017). Les connaissances acquises seront utiles à n'importe qui souhaite poursuivre dans la théorie des langages de programmation, la théorie de la démonstration, ou la théorie des catégories.


Bibliographie:

Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. 1992. Normal Forms and Cut-Free
Proofs as Natural Transformations. In in : Logic From Computer Science, Mathematical
Science Research Institute Publications 21. Springer-Verlag, 217–241.
<http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.811>

Paul Blain Levy. 2017. Contextual isomorphisms. In Proceedings of the 44th ACM SIGPLAN
Symposium on Principles of Programming Languages. ACM, 400–414.
<https://www.cs.bham.ac.uk/%7Epbl/papers/contextiso.pdf>

Guillaume Munch-Maccagnoni. 2017. Note on Curry’s style for Linear Call-by-Push-Value.
Draft. <https://hal.inria.fr/hal-01528857>

Accéder au sujet détaillé


SL308-78 Distributed Density Estimation despite Limited Communication  
Encadrement  
Encadrant : Emanuele NATALE(écrire)
Labo/Organisme : I3S (Laboratoire d'Informatique, Signaux
Ville : Nice

Description  
Within the context of Distributed Biological Algorithms (a recent sub-area of Distributed Computing that aims at investigating distributed algorithms found, or inspired by, biological systems), a lot of attention has been devoted to investigating how ant species perform various tasks [1]. An important problem has been how certain species of ants estimate the density of their conspecifics in some spatial area [2], a task which is considered necessary for the nest to coordinate in order to take some collective decisions (such as, migrating the nest to a new site). [2] provided important results in this direction, which also have relevant applications in mobile sensor networks.
More precisely, [2] essentially proves that a set of $m$ agents performing a random walk on a torus of size $n$ can estimate $m/n$ just by having each agent keep a statistics based on how many other agents stand on its current node; the surprising side of the result lies in the fact that, when two agents meet on a node, they are more likely to meet again in the very next time steps. By employing moment estimation techniques, the authors show that such stochastic dependencies can be handled and their effect on the estimator accuracy is negligible. The employed technique is of independent interest, since handling stochastic dependencies is, in general, a major challenge in the analysis of randomized algorithms.
The aim of this project is to address some shortcomings of the results in [2] and to generalize them to the natural setting in which the ability of the agents to count how many other agents lie on the same node is limited. In terms of the significance of the result regarding ants behavior, the proposed generalization naturally addresses the limited computational capacity of the ants. In terms of the technological applications, scenarios such as wireless sensor networks are often affected by collision phenomena and interferences which require the aforementioned assumption, i.e. the limited capacity of the agents to distinguish the presence of several different neighboring ones.
The student is expected to study and adapt the techniques in [2] in the setting briefly described above. Among the benefits that the intern will gain from the internship there are i) familiarity with fundamental tools in the analysis of randomized algorithms, namely probability concentration inequalities, ii) experience in understanding an high-quality research paper, in deconstructing its results and in trying to improve them, and iii) an understanding of the main issues and challenges in the area of distributed algorithms applied to collective behavior of natural systems.

[1] P. Fraigniaud, A. Korman, and Y. Rodeh, “Parallel Exhaustive Search Without Coordination,” in Proceedings of the Forty-eighth Annual ACM Symposium on Theory of Computing, New York, NY, USA, 2016, pp. 312–323.
[2] C. Musco, H.-H. Su, and N. A. Lynch, “Ant-inspired density estimation via random walks,” PNAS, vol. 114, no. 40, pp. 10534–10541, Oct. 2017.


Accéder au sujet détaillé


SL308-80 Schémas de signature basés sur les codes correcteurs d'erreurs  
Encadrement  
Encadrant : Tania RICHMOND(écrire)
Labo/Organisme : Inria/IRISA, équipe TAMIS
Ville : Rennes

Description  
Dans le contexte de la cryptologie post-quantique,
la cryptologie basée sur les codes correcteurs d'erreurs est l'une des plus prometteuses.
Le but de ce stage est de faire un état de l'art des schémas de signature basés sur les codes correcteurs d'erreurs, d'en extraire les principales idées de conception, de les comparer entre eux. Le travail consiste dans un second temps à analyser les attaques proposées dans la littérature et expliquer pourquoi elles ne
s'appliquent pas aux schémas plus récents.

Remarques:
Ce stage sera également suivi par Annelie Heuser
(CR CNRS dans la même équipe).


SL308-82 Attaque contre le schéma de chiffrement de McEliece  
Encadrement  
Encadrant : Tania RICHMOND(écrire)
Labo/Organisme : Inria/IRISA, équipe TAMIS
Ville : Rennes

Description  
La cryptographie dite post-quantique est un terme général qui englobe notamment la cryptographie basée sur les codes correcteurs d'erreurs.
Le premier schéma de chiffrement basé sur les codes est celui de McEliece, datant de 1978. Il est d'ailleurs le plus vieux schéma proposé au processus de standardisation du NIST pour le post-quantique.
Il existe des attaques par canaux auxiliaires contre ce schéma, qui visent à retrouver une partie de la clé privée. L'objectif de ce stage est de compléter ces attaques en retrouvant le reste de la clé privée. En d'autres termes, une fois la matrice de permutation retrouvée, il faut retrouver le polynôme de Goppa pour pouvoir décrire le code du même nom (faisant aussi partie de la clé privée).
Il s'agit essentiellement d'un travail d'implantation pour lequel le logiciel libre SageMath semble approprié.

Remarques:
Ce stage sera également suivi par Annelie Heuser
(CR CNRS dans la même équipe).


SL308-83 Vector Balancing  
Encadrement  
Encadrant : Alantha NEWMAN(écrire)
Labo/Organisme : G-SCOP
Ville : Grenoble

Description  

We propose to study the Komlos Conjecture, which is the following open problem in discrepancy theory.

Fix any n unit vectors in dimension d and let V denote a weighted sum of these n vectors, where each unit vector is weighted (multiplied) by a +1 or a -1. Then V is also a vector in dimension d. Consider the infinity norm of V, i.e., the entry in V with the largest absolute value. The Komlos Conjecture states that for any set of n unit vectors, there exists a +1,-1 weighting such that the infinity norm of the weighted sum is bounded by an absolute constant that is independent of d and n.

The goal of this stage is to investigate this (and maybe related) problems from experimental and algorithmic perspectives. Basic knowledge of some programming language (such as MATLAB) would be useful.

Remarques:
Possibilité de rénumération.


SL308-85 Ablation par cathéter radio-fréquences : algorithmes de krigeage pour la construction de méta-modèles  
Encadrement  
Encadrant : Michael LEGUÈBE(écrire)
Labo/Organisme : Institut Mathématiques de Bordeaux
Ville : Bordeaux (Talence)

Description  
voir PDF

Accéder au sujet détaillé

Remarques:
co-encadrant: Yves Coudière


SL308-88 Pijul, un système de contrôle de versions purement fonctionnel  
Encadrement  
Encadrant : Pierre-Étienne MEUNIER(écrire)
Labo/Organisme : Hamilton Institute, Maynooth University
Ville : Maynooth (Irlande)

Description  
Pijul est un système de contrôle de versions purement basé sur une théorie des patchs.

Alors que les systèmes existants (Git, SVN, Mercurial…) sont basés d'abord sur des "versions" divergentes réconciliées à coups d'heuristiques plus ou moins correctes, Pijul utilise une approche différente, qui a un certain nombre d'avantages :

- on peut par exemple prouver que les patchs de Pijul sont associatifs : appliquer un patch C après AB produit le même résultat qu'appliquer BC après A, ce qui n'est garanti dans aucun autre système (y compris Git).

- notre algorithme garantit aussi que deux patchs qui peuvent être produits en parallèle commutent toujours, ce qui implique que deux dépôts où le même ensemble de patchs a été appliqué dans deux ordres différents sont équivalents. Git garantit l'inverse de ça, en changeant les hashs des commits à chaque fois qu'on réordonne, ce qui force les utilisateurs à "rebaser" leurs changements, et peut avoir d'importantes conséquences sur de gros projets.

- enfin, les conflits dans Pijul sont un état normal, ce qui permet de les résoudre très simplement de plein de façons différentes. À l'inverse, Git (comme Mercurial ou SVN) n'a pas de représentation interne des conflits, et ne peut donc rien faire avant que l'utilisateur résolve le conflit.

Ce projet commence à intéresser quelques gros utilisateurs de Git (comme le projet NixOS, par exemple), ainsi qu'un certain nombre d'industriels. De par sa simplicité d'utilisation, Pijul pourrait également être utilisé par des organisations qui n'avaient pas jusqu'à maintenant la possibilité d'utiliser du contrôle de versions autrement que manuellement.

Les objectifs de ce stage peuvent être :

- de nous aider à formaliser notre théorie, et de prouver certains de nos algorithmes, éventuellement en Coq/Agda/…

- d'améliorer les performances de nos algorithmes, en particulier en termes d'espace disque.

Pijul est écrit en Rust. S'il n'est pas nécessaire de connaître ce langage pour candidater, il faut quand même avoir envie de l'apprendre pendant ou avant le stage.

Ce stage se déroulera à Maynooth, près de Dublin en Irlande.


Remarques:
Ce projet n'est pour le moment pas financé, mais peut déboucher sur des applications commerciales, y compris en 2019.


SL308-89 L’importance des tirages communs pour le consensus probabiliste  
Encadrement  
Encadrant : Matthieu PERRIN(écrire)
Labo/Organisme : LS2N
Ville : Nantes

Description  
Le consensus est un problème central en algorithmique distribuée, dans lequel des processus cherchent
à se mettre d'accord sur une valeur commune parmi celles proposées par chacun d'entre eux.
L'importance de ce problème vient du fait qu'il a été identifié comme universel pour
l'implémentation des objets partagés : si l'on possède une solution au consensus,
il est possible d'implémenter tous les objets possédant une spécification séquentielle.
Hélas, il n'existe pas d'algorithme déterministe implémentant le consensus dans un système
asynchrone (les processus ne s'exécutent pas à la même vitesse) et capable de résister
aux pannes, ne serait-ce que d'un seul processus.

Ce théorème d'impossibilité ne s'applique cependant pas aux algorithmes probabilistes.
Ceux-ci utilisent des variables aléatoires et doivent seulement terminer avec probabilité 1.
La plupart d'entre eux utilisent des tirages communs (common coins) pour assurer une terminaison en un nombre moyen de tirages constant :
tous les processus tirent la même séquence de variables aléatoires.
Le problème est que les common coins sont très difficiles à implémenter : ils nécessitent
plusieurs étapes de communication supplémentaires ou des hypothèses fortes sur l'asynchronie
des canaux de communication. Dans ce stage, nous proposons d'approfondir la question suivante :
le common coin est-il la meilleure abstraction pour implémenter le consensus efficacement ?

Plus de détails sont disponibles dans le sujet joint en PDF. De plus, n'hésitez pas à nous contacter pour en discuter !


Accéder au sujet détaillé

Remarques:
Co-encadrant : Achour Mostéfaoui


SL308-96 Deep learning with convolutional neural networks for holographic imaging of the human retina  
Encadrement  
Encadrant : Michael ATLAN(écrire)
Labo/Organisme : Institut Langevin CNRS UMR 7587
Ville : Paris

Description  
The retina relies on a finely tuned blood flow for its supply of metabolites and for disposal of waste products. A number of ocular and general diseases may affect the retinal circulation, and provoke arterial and venous occlusions. Monitoring retinal structure and vascularization is therefore crucial to understand the pathophysiology of visual loss in these diseases.

In this context, digital holographic techniques for tomography and angiography increasingly demonstrate clinical relevance. Our aim is to accelerate the transition to high resolution, high throughput, non-invasive structural and functional holographic imaging of the human retina in the hospital.

The clinical investigation center (CIC) of the Quinze-Vingts hospital, in collaboration with the Langevin Institute, has developed a unique expertise in the field of innovative high resolution holographic retinal imaging, and the evaluation of its medical use in a variety of ocular diseases.

Recording digital holograms on sensor arrays enables imaging with high sensitivity in low-light conditions, suitable for measurements in the retina. It was recently demonstrated that deep neural networks can be trained to find approximate solutions to image rendering in digital holography. The intern will design and train convolutional neural networks to determine whether they can outperform traditional hologram rendering. Training procedures will be done through Python scripts with Keras.


SL308-17 Utilisation du calcul GPU en recalage d’images médicales 3D  
Encadrement  
Encadrant : Laurent RISSER(écrire)
Labo/Organisme : Institut de Mathématiques de Toulouse
Ville : TOULOUSE

Description Sujet choisi par Baptiste ALLORANT  
Le but du stage sera de paralléliser les parties critiques d'un code C++ de recalage d'images médicales 3D à l’aide du calcul GPU (Graphic Programing Units), et d’évaluer l’impact de choix algorithmiques de parallélisation en terme de temps de calculs. Le recalage d’image 3D est un outil clé de l’analyse d’images médicales car il permet par exemple de quantifier les déformations d’organes d’un patient en IRM entre deux examens. Son utilisation sur données cliniques nécessite cependant de grosses ressources en termes de calculs, d’où l’intérêt du calcul GPU qui permet de paralléliser massivement du code de calcul numérique.

Le stage sera alors subdivisé en 3 parties : (1) découverte du recalage d'image et du calcul GPU, (2) re-implémentation de parties critiques d'un code C++ en CUDA, (3) évaluation de l'impact de la parallélisation GPU.

Il sera encadré par Laurent Risser (IR1 CNRS) à l'Institut de Mathématiques de Toulouse.

Accéder au sujet détaillé


SL308-63 Ordonnancement orienté mémoire dans le runtime StarPU  
Encadrement  
Encadrant : Loris MARCHAL(écrire)
Labo/Organisme : LIP, ENS Lyon
Ville : Lyon

Description Sujet choisi par Gabriel BATHIE  
Les plates-formes de calcul parallèle, utilisées par exemple pour effectuer des simulations numériques de grandes tailles, deviennent de plus en plus complexes: utilisation d'accélérateurs de calcul, hiérarchies mémoires profondes, combinaison de mémoires partagées et distribuées. Pour tirer partie de leur puissance, il devient nécessaire de s'appuyer sur des ordonnanceurs légers, tels que le runtime StarPU, développé (entre autres) par Samuel Thibault. Une application de calcul est alors décrite comme un graphe de tâches, dont les arêtes modélisent les dépendances, et l'ordonnanceur s'efforce de placer les tâches disponibles sur les différents coeurs de calcul pour optimiser les performances. Entre autres problèmes à résoudre pour bien ordonnancer un tel graphe se pose la question de la mémoire: il faut à tout prix éviter la situation de pénurie de mémoire, au risque de voir l'exécution échouer (ou tout au moins obtenir des performances largement dégradées).

Des solutions à ce problème ont été proposées. Récemment, nous avons proposé une méthode qui ajoute des dépendances au graphe de tâches afin que toute exécution ne dépasse pas une quantité de mémoire donnée. Cette méthode a le grand avantage de ne pas brider l'ordonnanceur plus que nécessaire, afin qu'il puisse s'adapter aux conditions réelles au moment de l'exécution. Malheureusement, la complexité de la solution et le grand nombre de dépendances ajoutées rend cette méthode peu utilisable en pratique.

L'objectif de ce stage est d'améliorer cette méthode, en limitant les garanties à fournir: au lieu de s'assurer que toute exécution ne dépasse pas la mémoire, il suffit en effet de garantir l'absence de situations d'interblocage (deadlock) à cause la mémoire: les runtimes tels que StarPU savent bloquer une tâche demandant de la mémoire tant que celle-ci n'est pas disponible. Ce méchanisme devrait permettre de rajouter bien moins de nouvelles dépendances au graphe.

Le travail demandé pendant se stage consistera en plusieurs étapes.
- Modéliser le problème sous forme d'un problème de graphe, en choisissant la modélisation mémoire qui paraît la plus pertinente et en exprimant l'objectif poursuivi comme une propriété du graphe.

- Proposer des solutions algorithmiques pour résoudre ce problème, en cherchant à réduire la complexité de ces solutions.

- Tester l'efficacité des solutions proposées d'abord par une campagne de simulations sur des graphes connus.

- Implanter certaines de ces solutions dans le runtime StarPU.


Accéder au sujet détaillé

Remarques:
Stage co-encadré par Yves Robert et Samuel Thibault


SL308-81 Modèles catégoriques de la logique linéraire différentielle.  
Encadrement  
Encadrant : Assia MAHBOUBI(écrire)
Labo/Organisme : Inria & Université de Nantes
Ville : Nantes

Description Sujet choisi par Esaie BAUER  
Ce stage consiste en une étude des axiomatisations catégoriques des modèles de la Logique Linéaire Différentielle (DiLL). Il vise à une synthèse de ces différentes axiomatisations sous l'angle de la dualité. La logique linéaire est un système de preuve formelle transportant les intuitions de l'algèbre linéaire et servant de cadre à de nombreux developements en vérification, recherche de preuve et sémantique des langages de programmation. DiLL [1] est une extension de la logique linéaire permettant la linéarisation des preuves. En particulier, les règles d'élimination des coupures se comprennent à travers des intuitions d'analyse réelle et de différentiation de fonctions. Néanmoins, différentes définitions de la logique linéaire différentielle cohabitent et nous chercherons en particulier à unifier celle de Fiore [2] et de celle récemment donnée par Ehrhard [3]. Cette recherche est motivée par la mise en évidence de modèles concrets [4] [5] de la logique linéaire différentielle où la dualité des modèles de Ehrhard est centrale mais qui utilisent les constructions de Fiore [2]. Suivant les préférences de la ou du stagiaire, on pourra aborder le travail d'un point de vue syntaxique, catégorique, ou du point de vue de l'analyse fonctionnelle. Ce stage sera l'occasion d'apprendre des bases de théorie de la preuve, de logique linéaire et de sémantique dénotationnelle. Il convient à une personne ayant un goût pour les fondements théoriques de l'informatique ou ayant un parcours mixte maths/info. Il se déroule dans la jeune et dynamique équipe Gallinette à Nantes, centrée thématiquement sur la théorie des types.



[1] Thomas Ehrhard, Laurent Regnier: Differential interaction nets. Theor. Comput. Sci. 364(2): 166-195 (2006).
[2] Marcelo P. Fiore: Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic. TLCA 2007: 163-177.
[3] Thomas Ehrhard : An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science 28(7): 995-1060 (2018).
[4] Marie Kerjean: A Logical Account for Linear Partial Differential Equations. LICS 2018: 589-598.
[5] Marie Kerjean, Jean-Simon Lemay : Higher-Order Distributions for Differential Linear Logic, Fossacs 2019.


Remarques:
Stage co-encadré par Marie Kerjean, marie.kerjean@inria.fr .

Possibilité de rémunération.


SL308-77 Mots incomplétables minimaux  
Encadrement  
Encadrant : Sandrine JULIA(écrire)
Labo/Organisme : I3S
Ville : Sophia Antipolis

Description Sujet choisi par Gaetan BERTHE  
Un langage X de mots finis sur un alphabet A est dit complet si tout mot sur A peut être recouvert par une concaténation de mots de X. Un mot pour lequel ce n’est pas possible est dit incomplétable. Parmi eux, on distingue les mots minimaux incomplétables qui le sont à une lettre près.
Il existe des problèmes ouverts sur les ensembles complets. Par
exemple : quelle est la complexité exacte du problème de décider si un ensemble donné est complet ? Si un ensemble n'est pas complet, quelle est la longueur du plus court mot incomplétable ? Ces problèmes sont reliés au problème du mot synchronisant dans les automates finis [CaAl17].

Quand X est fini, le problème est de trouver une borne supérieure
sur la longueur du plus court mot minimal incomplétable en fonction de k, la longueur maximale des mots de X.
Bien que la conjecture de A. Restivo [Res81] qui énonce qu’il existe une borne supérieure en 2k^2 soit contredite ([GuPr11]),
le problème de l’existence d’une borne quadratique demeure [RSX12]. Dans l’étude [JMP17], un nouvel algorithme a permis de pousser les calculs plus avant au point qu’une borne quadratique semble compromise.

L'étudiant devra prendre connaissance de la bibliographie relative aux mots incomplétables puis appréhender le problème dans le cas où X est un ensemble fini. D’une part, les mots incomplétables ont été caractérisés en introduisant un nouvel ensemble Z fait de mots qui contribuent à stopper les factorisations sur X*. L’étude de cet ensemble mérite d’être approfondie. D’autre part, il serait intéressant d’étudier ce problème pour différentes classes de langages comme les différents codes pour laquelle la combinatoire est réduite. Différentes pistes s’offrent à nous pour y parvenir : approche théorique, étude statistique, exploration de graphes d’automates etc.
L’étudiant pourra choisir et orienter son stage en fonction de ses aspirations et de ses goûts.

Références
[CaAl17] A. Carpi et F. D’Alessandro. On incomplete and synchronizing finite sets, Theoretical Computer Science, 664 : 67-77, 2017.
[GuPr11] V. Gusev et E. Pribavkina. On non-complete sets and Restivo's conjecture. DLT 2011, LNCS 6795 : 239-250, 2011.
[JMP17] S. Julia, A. Malapert, et J. Provillard. A synergic approach to the minimal uncompletable words problem. Journal of Automata, Languages and Combinatorics, 22(4):271--286, 2017.
[Res81] A. Restivo. Some remarks on complete subsets of a free monoid. Quaderni de La Ricerca Scientifica, CNR Roma, 109 : 19-25, 1981.
[RSX12] N. Rampersad, J. Shallit et Z. Xu. The Computational Complexity of Universality Problems for Prefixes, Suffixes, Factors, and Subwords of Regular Languages. Fundam. Inform.,volume 116, 1-4 : 223-236, 2012.

Remarques:
Ce stage sera co-encadré avec Julien Provillard.


SL308-66 Réseaux linéaires sur nombres de nim  
Encadrement  
Encadrant : Christophe PAPAZIAN(écrire)
Labo/Organisme : I3S - Université de Nice Sophia
Ville : Sophia Antipolis

Description Sujet choisi par Jules BERTRAND  
Les réseaux linéaires sont des graphes d’automates finis représentant un réseau synchrone dont chaque noeud change d’état selon une fonction linéaire de l’état de ses voisins. La dynamique de ce système complexe peut être analysée grâce à des techniques algébriques, en particulier la décomposition des matrices sous forme normale de Frobenius si l’état appartient à un corps algébrique. De nombreuses questions restent ouvertes sur d’autres structures algébriques.
Les nombres de nim (nimbers) sont des nombres représentant des stratégies dans les jeux impartiaux à information complète et à deux joueurs. Introduits par J.H.Conway, ils permettent de calculer efficacement les coups gagnants dans de nombreux jeux combinatoires finis en faisant du calcul sur les entiers ou infini en utilisant les ordinaux de la théorie des ensembles. Munis naturellement d’une addition et d’une multiplication, les nombres de nim forment un corps et ont alors de nombreuses propriétés algébriques particulières.
Le but de ce stage est d’étudier le comportement des réseaux linaires dont les état sont des nombres de nim choisis sur une partie des ordinaux dénombrables. En particulier, étudier les dynamiques possibles de tels réseaux, la complexité algorithmique des simulations et de l’analyse d’un tel réseau et les propriétés d’universalité de ce modèle.

[1] Enrico Formenti, Luca Manzoni, and Antonio E. Porreca. Fixed points and attractors of reaction systems. In Arnold Beckmann, Erzsébet Csuhaj-Varjú, and Klaus Meer, editors, Language, Life, Limits - 10th Conference on Com- putability in Europe, CiE 2014, Budapest, Hungary, June 23-27, 2014. Pro- ceedings, volume 8493 of Lecture Notes in Computer Science, pages 194–203. Springer, 2014.
[2] Mathilde Noual. Updating Automata Networks. Phd thesis, Ecole Normale Supérieure de Lyon, 2012.
[3] Christopher Frei and Sophie Frisch. Non-unique factorization of polynomials over residue class rings of the integers. Comm. Algebra, 30:1482—1490, 2011. [4] John Horton Conway, On Numbers and Games, 1976, ISBN 978-1568811277

Remarques:
Le stage sera co-encadré par Enrico Formenti.
Une rémunération pour un étudiant non salarié est possible.


SL308-24 Sémantique des blocs inline assembleurs x86 dans du code C  
Encadrement  
Encadrant : Jérôme FERET(écrire)
Labo/Organisme : DI ENS
Ville : Paris

Description Sujet choisi par Jrome BOILLOT  
# Sujet

Pour garantir le bon fonctionnement d'un système critique, il faut en certifier chaque couche. On s'intéresse souvent au logiciel final. C'est un premier pas indispensable, mais c'est incomplet. En effet, il faut s'assurer du bon fonctionnement du système d'exploitation (le cas échéant), du matériel etc.. Souvent, on est réduit à faire confiance au matériel, faute d'implémentation à certifier, mais on peut tout à fait s'intéresser à l'OS.

Le cas d'étude est l'analyse d'un OS embarqué. En particulier, on veut prouver l'isolation de la mémoire.

La première étape en ce sens est le support dans Astrée de programmes C comportant des blocs de code écrit en assembleur x86.

Le C a pour but d'être portable, donc indépendant de la plateforme. L'assembleur est au contraire, éminemment dépendant du matériel. Un OS ne peut donc pas se passer d'assembleur pour utiliser les fonctionnalités dépendantes du matérielles et qui sont hors du cadre du C. Tout n'a pas besoin d'être en assembleur. La majorité des opérations et du contrôle de flot se formule aussi bien en C et reste plus clair et moins sujet à erreurs. C'est pourquoi, l'assembleur n'est présent que sous forme de petits bouts de code épars insérés au sein du code C, dont l'abstraction est confortable.

Pour être capable de faire une analyse sur ces codes, il faut avant tout avoir une sémantique de ces langages.

La sémantique du C est décrite par sa norme, et celle de l'assembleur par la documentation des processeurs. Mais il n'existe pas de description précise des interactions entre le C et l'assembleur. C'est en effet un sujet délicat puisqu'il faut faire des hypothèses supplémentaire sur le C pour qu'il s'interface correctement. Il faut par exemple connaître (plus ou moins précisément) la position des variables dans la mémoire, ou encore, connaître la structure de la pile. Certaines de ces hypothèses existent déjà sous forme d'ABI (notamment les conventions d'appel). D'autres dépendent énormément de la compilation, et fonctionnent en particulier dans le cas d'une compilation simple (style dirigé par la syntaxe), peu optimisante. D'autres part, une description aussi précise de ces hypothèses que l'ABI n'est pas toujours nécessaire. Parfois, une abstraction de celles-ci peut suffire à garantir que le code s'exécute correctement.

Les interactions peuvent prendre différentes formes. La plus simple consiste à modifier les variables du C dans un bloc assembleur. Les interactions les plus complexes agissent sur le flot de contrôle. Par exemple, avec un retour précoce de la fonction ou, pire, en modifiant l'adresse de retour.

Le but du stage est de décrire cette sémantique, trouver les hypothèses raisonnables et automatiser cette déduction dans la mesure de ce qui apparaîtra possible.


# Mission

Ce sujet pose un certain nombre de questions peu explorées. Ce qui signifie qu'il est possible de choisir un sujet très théorique ou au contraire plein d'implémentations subtiles ou encore un compromis entre les deux.

Les missions d'un stage équilibré entre théorie et implémentation peuvent être :
- choisir un modèle pour décrire l'état mémoire lors de l'exécution d'un programme C avec de l'assembleur inline ;
- comprendre la sémantique des blocs inline et trouver les hypothèses nécessaire de compilation au bon fonctionnement du code cible ;
- implémenter un interpréteur d'une partie (très) restreinte du C qui gère les blocs assembleurs, notamment le flot de contrôle de l'assembleur (sans hypothèses sur les adresses absolues concrètes) ;
- inférer automatiquement les règles nécessaires à l'exécution d'un programme.

Comme on est toujours dans le cadre de l'embarqué, il y a d'autres questions adjacentes qui sont tout aussi intéressantes. Par exemple, comment prouver que la pile est convenablement vidé pour ne pas laisser de données inutiles alors que le flot de contrôle du C est détourné par de l'assembleur. Ou... les possibilités sont colossales !


Accéder au sujet détaillé

Remarques:
Gratification minimale pour les auditeurs
Co-encadrement par Marc Chevalier


SL308-79 Analyse d'Efficacité de Services en Pi-Calcul  
Encadrement  
Encadrant : Romain DEMANGEON(écrire)
Labo/Organisme : Laboratoire d'Informatique de Paris 6
Ville : PARIS

Description Sujet choisi par Amel CHADDA  
Ce stage a pour but l'étude d'une analyse d'efficacité pour des réseaux de services décrits dans le formalisme du pi-calcul. L'analyse en question a été décrite dans une publication récente et un premier prototype a été produit. A l'aide d'un système de types et de contraintes syntaxiques, l'analyse décide si un processus
du pi-calcul modélise un réseau de service "efficace" (génération de messages polynomiale en la taille de la requête initiale).

L'objectif du stage est d'étudier cette analyse et son implémentation et de proposer des améliorations d'efficacité (optimiser les algorithmes qui parcourent et manipulent des types et des termes du pi-calcul) et d'expressivité (pouvoir reconnaître un plus grand nombre de processus du pi-calcul efficaces) pour le prototype et l'analyse
elle-même.

(cf. sujet détaillé)

Accéder au sujet détaillé

Remarques:
Possibilité de rémunération possible (mais peu probable, à discuter).


SL308-73 Un générateur d'opérateurs sur les posits  
Encadrement  
Encadrant : Florent DE DINECHIN(écrire)
Labo/Organisme : CITI, INSA Lyon
Ville : Lyon

Description Sujet choisi par Oregane DESRENTES  
Les posits (https://posithub.org/) sont une alternative, proposée récemment [1], au format flottant habituellemnt utilisé pour représenter des réels.
La jeune littérature les concernant est d'une mauvaise foi remarquable, mettant en avant les avantages de ce format mais ignorant ses défauts.
Par exemple, elle rapporte un certain nombre d'expériences remplaçant, dans une applications donnée, les flottants par des posits de même taille, et montrant que la la qualité numérique des résultats est augmentée [2]. C'est sans doute vrai (même s'il faudrait se garder de le généraliser à toutes les applications [3]), mais les opérations posit utilisées nécessitent des registres internes de très grands formats, et il est légitime de mettre en rapport le bénéfice de cette solution avec son coût.

L'objectif de ce stage est donc de fournir un outil qui manque pour permettre une comparaison complète et sereine (non biaisée) des mérites comparés des posits et des flottants: un générateur open-source de circuits implémentant le standard posit. Ce générateur sera intégré au projet FloPoCo (http://flopoco.gforge.inria.fr), qui supporte déjà les flottants et l'arithmétique logarithmique, et on cherchera à optimiser les opérateurs posit autant que les opérateurs flottants.

FloPoCo étant un générateur de VHDL écrit en C++, un goût pour ces deux langages est nécessaire.

Bibliographie:
[1] https://posithub.org/docs/posit_standard.pdf
[2] https://posithub.org/conga/2018/docs/1-Peter-Lindstrom.pdf
[3] https://hal.inria.fr/hal-01959581


SL308-46 Application des méthodes d'optimisation basées mesures à la surapproximation de zonotopes, en Caml  
Encadrement  
Encadrant : Pierre-Loic GAROCHE(écrire)
Labo/Organisme : ONERA/DTIS
Ville : Toulouse

Description Sujet choisi par Loic DUBOIS  
Les hiérarchies de Lasserre sont des solutions élégantes, avec des résultats forts de convergence en volume, pour calculer des solutions approchées de problèmes d’optimisation. Le problème est exprimé dans un espace fonctionnel (de dimension infinie) puis projeté sur une base polynomiale de degré fixé.

Nous nous proposons ici d’effectuer un changement de base polynomiale dans l’expression des contraintes du problème d'optimisation. L'utilisation des polynômes de Hermite semble plus adaptée pour traiter des problèmes sans faire d'hypothèse de compacité sur les ensembles manipulés.

L'objectif du stage est de développer une librairie en Caml pour effectuer ces changements de base et l'utilisation de l'optimisation convexe sur ces problèmes. En particulier, il vous sera donc demandé :
• d’écrire une librairie en Caml pour la manipulation de polynômes de Hermite (pour gérer les opérations
d’addition et de multiplication);
• d’exprimer la matrice de Gram pour les polynômes de Hermite;
• de traduire le problème en un problème d’optimisation polynomiale;
• puis de faire appel à un solveur d’optimisation convexe;
• enfin, de traiter un exemple simple de surapproximation de zonotopes par une ligne de niveau polynomiale.

Accéder au sujet détaillé


SL308-42 Échantillonnage rapide de surfaces 3D in the wild  
Encadrement  
Encadrant : David COEURJOLLY(écrire)
Labo/Organisme : LIRIS
Ville : Villeurbanne

Description Sujet choisi par Yann-Situ GAZULL  
Dans de nombreuses applications de traitement et de modélisation de géométries 3D, la distribution de points équitablement répartis sur une surface est une étape indispensable.

Dans la littérature, lorsqu'il s'agit d'échantillonner un domaine plan, cette distribution équitable des points se caractérise par des propriétés statistiques (uniformité, basse discrépance...) [Lemieux] ou spectrales (pas alignements, distance moyenne...) [Pilleboue15]. De nombreux articles et outils logiciels existent maintenant sur ces domaines (e.g. utk). Sur des surfaces 3D, l'analyse diffère un peu mais plusieurs auteurs ont proposé des outils permettant de générer des points et de les analyser ([Wei11] [Ahmed16]...). Ces outils utilisent principalement, soit une paramétrisation de la surface, soit des propriétés différentielles locales de cette dernière pour déformer un échantillonnage uniforme (planaire) et ainsi l'adapter à la géométrie.


Ces outils ont un prérequis important qui est que la surface doit être bien définie et topologiquement correcte (et donc porter une notion de métrique intrinsèque utilisée notamment pour la distribution équitable des points).

L'objectif du stage est de s'intéresser à des surfaces complexes (plusieurs composantes connexes, auto-intersections, jonctions complexes...), voire une soupe de triangles, avec quand même le prérequis que ces surfaces correspondent à des approximations d'une surface sous-jacente topologiquement correcte. Ce type d'artefacts topologiques apparaît assez souvent en modélisation 3D lorsque l'on s'intéresse uniquement à l'aspect de la surface visible externe (pour du rendu par exemple).




L'objectif est donc de proposer des outils d'échantillonnage sur ce type de surfaces. De nombreuses options sur possibles (étape de reconstruction ou de réparation de surfaces, estimation de propriétés intrinsèques via plongement ambiant, exploitation de la paramétrisation UV de texture de l'objet 3D si celle-ci est disponible [Prada18]...).

Dans un premier temps, on pourra s'intéresser à un échantillonnage mixte de la géométrie et d'une estimation de la surface sous-jacente obtenue par une information stable d'intérieur - extérieur [Jacobson13] [Barill18].



Références

[Lemieux] Chrisitiane Lemieux, Monte Carlo and Quasi-Monte Carlo Sampling, Springer, 2009.
[Pilleboue15] Adrien Pilleboue, Gurprit Singh, David Coeurjolly, Michael Kazhdan, Victor Ostromoukhov. Variance Analysis for Monte Carlo Integration. ACM Transactions on Graphics (Proceedings of SIGGRAPH), 34(4):14, August 2015.
[Wei11] Wei, Li-Yi, and Rui Wang. “Differential domain analysis for non-uniform sampling. ACM Transactions on Graphics (TOG). Vol. 30. No. 4. ACM, 2011.
[Ahmed16] Ahmed, Abdalla G.M.; Guo, Jianwei; Yan, Dong-Ming; Franceschi, Jean-Yves; Zhang, Xiaopeng; Deussen, Oliver, A Simple Push-Pull Algorithm for Blue-Noise Sampling, IEEE Transactions on Visualization and Computer Graphics, 2016.
[Prada18] F. Prada, M. Kazhdan, M. Chuang, and H. Hoppe, Gradient-Domain Processing within a Texture Atlas (Slides, Source and Executables), SIGGRAPH (2018Vol. 37, No. 4)
[Jacobson13] Jacobson, Alec, Ladislav Kavan, and Olga Sorkine-Hornung. “Robust inside-outside segmentation using generalized winding numbers.” ACM Transactions on Graphics (TOG) 32.4 (2013): 33.
[Barill18] BARILL, G., DICKSON, N. G., SCHMIDT, R., LEVIN, D. I., & JACOBSON, A. Fast Winding Numbers for Soups and Clouds. Siggraph, ACM TOG, 2018


Accéder au sujet détaillé

Remarques:
Le stage se déroulera au sein du laboratoire LIRIS (bat. Nautibus) avec gratification.

Encadrant : David Coeurjolly

Compétences requises : C++, cmake, git.


SL308-84 Calculs symboliques et preuves formelles en théorie algébrique des nombres  
Encadrement  
Encadrant : Assia MAHBOUBI(écrire)
Labo/Organisme : Inria -- Université de Nantes
Ville : Nantes

Description Sujet choisi par Paul GENEAU-DE-LA-MARLIERE  
L’objectif de ce stage est de concevoir et de réaliser des bibliothèques de mathématiques formalisées en théorie algébrique des nombres, à l’aide de l’assistant de preuve Coq. On s’intéressera en particulier à la vérification d’algorithmes de calcul symbolique (aussi appelé calcul formel). L’objectif à terme est de fournir des implantations de ces algorithmes dont la correction est vérifié formellement, fournissant ainsi le plus haut niveau de garantie possible.

Dans le cadre de ce stage, on se propose d’étudier les algorithmes de calcul des nombres de classes des corps quadratiques.

Ce travail de formalisation en Coq s’appuiera sur les bibliothèques Mathematical Components, et suivra la méthodologie de formalisation qu’elles mettent en œuvre. Ces bibliothèques contiennent une base de vocabulaire en algèbre commutative, algèbre matricielle, etc. qui permettra de se concentrer sur les objets mathématiques propres au sujet du stage. Les aspects calculatoires, eux, sont plus prospectifs.

Accéder au sujet détaillé

Remarques:
Ce stage sera co-encadré à distance par Sander Dahmen (département de mathématiques, VU Amsterdam). Des réunions hebdomadaires par visio-conférence sont prévues avec lui. Une visite (financée) d’une semaine environ du ou de la stagiaire au département de mathématiques de la VU Amsterdam pendant le stage est également envisagée.

Rémunération possible.


SL308-29 Version discrète du partage du gâteau  
Encadrement  
Encadrant : Frédéric MEUNIER(écrire)
Labo/Organisme : CERMICS
Ville : Champs-sur-Marne

Description Sujet choisi par Matthieu HERVOUIN  
Les problématiques de division équitable constituent un domaine de recherche actif, à la frontière des mathématiques discrètes et de la théorie du choix social. Un des principaux sujets dans ce domaine est celui du partage "sans-envie" d'un gâteau. Il s'agit de découper un gâteau, identifié à l'intervalle [0,1], en des parts connexes et d'attribuer ces dernières à des joueurs ayant des préférences différentes de façon à ce qu'aucun joueur ne soit jaloux d'un autre.

Des conditions très faibles assurent l'existence de tels partages sans-envie. Les preuves utilisent entre autre la possibilité de découper le gâteau n'importe où. En revanche, dans la version discrète du problème, il n'est possible de couper le gâteau qu'en un nombre fini de points (ce qui peut correspondre par exemple à un partage sans-envie d'un collier) et un partage sans-envie n'existe alors pas forcément. On peut cependant trouver des approximations de partage sans-envie. Dans un modèle particulier d'approximation appelé EF1 ("envy-free up to one boundary item"), l'existence d'un partage a été montrée pour au plus 4 joueurs, mais est totalement ouverte pour 5 joueurs et plus.

L'objectif du stage est d'étudier la version discrète du partage sans-envie du gâteau et plus spécifiquement de progresser dans la compréhension de la question ouverte sur les partages EF1. Des questions algorithmiques afférentes, nombreuses dans ce contexte, pourront aussi être abordées.

Remarques:
Indemnités de stage possibles


SL308-37 Manipulation d’arbres contraints pour lignes de produits logiciels  
Encadrement  
Encadrant : Pierre BOURHIS(écrire)
Labo/Organisme : Spiral CRIStAL
Ville : Lille

Description Sujet choisi par Thibault MARETTE  
Contexte : les arbres contraints sont massivement utilisés dans les lignes de produits logiciels car ils permettent de décrire les différentes configurations possibles d’un logiciel. Une configuration du logiciel correspond alors à une sélection de certains nœuds de l’arbre respectant les contraintes associées à l’arbre (par exemple, la sélection d’un nœud implique la non-sélection d’un autre nœud). Différents types d’opérations peuvent être effectués sur l’arbre : compter/lister le nombre de configurations, détecter les nœuds inutilisés, vérifier la validité d’une configuration, etc. Surprenant, ces arbres sont aussi étudiés en bases de données pour représenter des données incomplètes représentées sous forme d’arbres.

Problématique : dans le cadre de grands logiciels, ces opérations peuvent être difficiles voire impossible à réaliser du fait de l’explosion combinatoire qui découle de la taille de l’arbre et des contraintes associées. Les approches actuelles sont généralement basées sur des solveurs (BDD ou SAT notamment) qui ne permettent pas le passage à l’échelle. Cependant, d’autres techniques de manipulation d’arbres issues des bases de données et la traduction des contraintes dans circuits dont la manipulation est tractable telles que les DDNNF [en dire plus] semblent prometteuses et laisse entrevoir la possibilité de repousser voire d’éliminer ce problème d’échelle.


Travail à réaliser : dans un premier temps, le travail consistera à réaliser une traduction d’arbre contraint vers une DDNNF, ainsi que l’implémentation permettant d’automatiser cette traduction. Par la suite, des expériences seront menées pour comparer les performances obtenues en effectuant différentes opérations sur ces arbres contraints avec deux approches différentes (e.g., SAT vs DDNNF). Suivant l’avancement du projet, le travail pourra ensuite porter sur des opérations envers des arbres contraints probabilistes et/ou sur l’évolution (la mise à jour) de ces arbres.


Remarques:
Ce travail sera co-encadre avec Clement Quinton (clement.quinton@univ-lille.fr)

Ce stage peut etre remunere. Les frais accomodations peuvent etre pris en charge par l equipe Spirals.


SL308-58 Formal modelling and analysis of the biological mechanisms involved in Diabete type 2  
Encadrement  
Encadrant : Cédric LHOUSSAINE(écrire)
Labo/Organisme : CRIStAL
Ville : Villeneuve d'Ascq

Description Sujet choisi par Alexandre MARTHE  
This project is proposed as part of a collaboration between the bioComputing
team, biochemists from the Arab American University of Jenin (Palestine) and
physicians from the European Genomic Institute for Diabetes (Lille). The global
topic is the *modelling and analysis of the biological mechanisms involved in
Diabete type 2*, a disease due to resistance to insulin action, whose worldwide
prevalence rapidly rises. Our partners of the project focus on plant extracted
molecules (in particular from Basil) [1], and on gastric bypass surgery [2].
They showed that these have efficient anti-diabetic effects.

However, their causal relationship with diabete remains largely unclear.
Revealing how basil molecules can circumvent deficient insulin response due to
diabete [3], could lead to new drug designs. Also, one may conceive less invasive
therapies from the understanding of the effects of gastric bypass on intestinal
glucose absorption.

In this large and ambitious project, the bioComputing team is involved in two
main tasks : *modelling* and *analysis*. The student will focus on either
modelling or analysis, according to the candidate's preferences. *The modelling
task*, which requires a strong interest in biology, consists in elaborating a
*formal computational model* of either the molecular insulin pathway or
intestinal absorption. The bioComputing team uses languages based on *abstract
biochemical reactions*, similar to Petri Nets [9] and BioCHAM language [4], that
let one choose the appropriate abstraction level according to biological
knowledge, relevance of details and planed analyses. The model must be validated
against biological data. Once completed, its characteristics will give hints on
the kind of formal analyses that can be conducted.

For the *analysis task*, a strong interest in the *formal semantics of
programming languages* and *logic* is required. We aim at designing new
algorithms that, given a partial reaction network, infer the missing reactions,
such that the resulting completed model can reproduce a observed behavior. More
precisely, these algorithms will operate on
1) a partial model given as a set of reactions,
2) an output objective (i.e. the observed behavior) represented by a
particular reaction of the model for which one wants to observe an increase
or decrease of its activity,
3) a least set of reactions that represent new behaviors that one may add to
the model.
The analysis should determine which behaviors are more likely to reach the
output objective. The team already develops methods based on *abstract
interpretation* for models lacking kinetic information [5,6], but this project
is more generaly open to *logical approaches to AI* [10]. The analysis will be
applied in the project, initially using a very rough formal model of insulin
signaling taken from the litterature, with GLUT4 insertion in the membrane as
the objective [3].

References

[1] /In vitro evaluation of anti-diabetic activity and cytotoxicity of
chemically analysed Ocimum basilicum extracts/. Kadan, Sleman and Saad,
Bashar and Sasson, Yoel and Zaid, Hilal. /Food Chemistry/ 196:1066-1074, 2016.

[2] /Bile Diversion in Roux-en-Y Gastric Bypass Modulates Sodium-Dependent Glucose Intestinal Uptake./
Baud, G., Daoudi, M., Hubert, T., Raverdy, V., Pigeyre, M., Hervieux, E., et al. (2016).
Cell Metabolism, 23(3), 547–553. http://doi.org/10.1016/j.cmet.2016.01.018

[3] /Update on GLUT4 Vesicle Traffic: A Cornerstone of Insulin
Action/. Jaldin-Fincati J, Pavarotti M, Frendo-Cumbo S, Bilan P, Klip A. /Trends
in Endocrinololgy and Metabolism/ 28(8):597-611, 2017.

[4] /Modelling and querying interaction networks in the biochemical abstract
machine BIOCHAM/. Fages F, Soliman S and Chabrier-Rivier N. /Journal of
Biological Physics and Chemistry/ 4(2):64-73, 2004.

[5] /Modeling Leucine’s Metabolic Pathway and Knockout Prediction Improving the
Production of Surfactin, a Biosurfactant from Bacillus Subtilis/ Coutte F,
Niehren J, Dhali D, John M, Versari C and Jacques P. /Biotechnology Journal/
10(8):1216-34, 2015.

[6] Mathias John, Mirabelle Nebut, Joachim Niehren. /Knockout Prediction for
Reaction Networks with Partial Kinetic Information/. 14th International
Conference on Verification, Model Checking, and Abstract Interpretation. 2013.

[7] /Quasi-Steady-State Analysis based on Structural Modules and Timed Petri Net
Predict System’s Dynamics: The Life Cycle of the Insulin Receptor/ Scheidel, J.,
Lindauer, K., Ackermann, J., & Koch, I. Metabolites, 5(4), 766–793, 2015.

[8] /Modeling Integrated Cellular Machinery Using Hybrid Petri-Boolean Networks/
Berestovsky, N., Zhou, W., Nagrath, D., & Nakhleh, L. PLoS
Computational Biology, 9(11). 2013.

[9] CHAOUIYA, Claudine. /Petri net modelling of biological networks/. Briefings
in bioinformatics, vol. 8, no 4, p. 210-219. 2007.

[10] François Fages. AI in Biological Modeling. In A Guided Tour of Artificial
Intelligence Research. Springer-Verlag, 2017.


Accéder au sujet détaillé


SL308-91 Analyse statique pour aider la détection d'états équivalents dans SimGrid  
Encadrement  
Encadrant : Emmanuelle SAILLARD(écrire)
Labo/Organisme : Inria
Ville : Talence

Description Sujet choisi par Firmin MARTIN  
Comprendre et analyser le comportement d'une application HPC est un travail difficile. Il existe des initiatives, comme l'Inria Project Lab (IPL) HAC-SPECIS, qui vise à trouver des solutions pour aider les programmeurs à corriger et optimiser leurs applications. Une des pistes envisagées de cet IPL est de simuler l'exécution d'un programme afin de prédire son comportement pour une valeur fixée des données d'entrées. SimGrid est un outil qui utilise cette méthode pour détecter des erreurs dans les applications distribuées. Il est basé sur une approche dite de model checking. Le model checking est une technique de vérification formelle qui permet de déterminer si un modèle donné (le système lui-même ou une abstraction de celui-ci) satisfait une spécification. Cette approche repose sur des méthodes d'exploration de l'espace d'états du système pour démontrer qu'un état (ou un ensemble d'états) indésirable(s) est accessible ou inaccessible. Pour cela, l'ensemble des exécutions possibles du système est déterminé, à partir d'un état initial. L'exploration des états s'effectue ensuite jusqu'à ce qu'une violation de propriété soit détectée ou bien jusqu'à l'exploration complète de l'espace d'états. En pratique, le model checking est limité par la taille des systèmes étudiés. Pour pallier l'explosion combinatoire de l'espace d'états d'un système, des techniques existent pour réduire la taille des modèles. Par exemple, en détectant les états qui peuvent être considérés comme equivalents.

Par le biais d'une analyse dite statique, le compilateur est en mesure de fournir des informations relatives au comportement d'un programme. C'est par exemple le cas des analyses de flot de données, qui ont la possibilité de détecter si à partir d'un point du programme, la valeur d'une variable sera utilisée. Ce genre d'analyse peut aider la vérification formelle à réduire l'espace d'états en détectant les états sémantiquement équivalents.

L'objectif de ce stage est de développer une analyse statique visant à améliorer la détection des états equivalents dans SimGrid. Pour cela, on cherchera à:

1. Détecter et mettre à 0 toutes les variables non initialisées d'un programme (quelque soit leur type)

2. Détecter et mettre à 0 les variables mortes

L'analyse sera développée dans le compilateur LLVM sous forme d'une passe. La dernière phase du stage sera dédiée à la validation de la passe sur des cas tests.


SL308-20 Évaluation efficace de motifs réguliers pour l’extraction de données  
Encadrement  
Encadrant : Antoine AMARILLI(écrire)
Labo/Organisme : Laboratoire LTCI, Télécom ParisTech
Ville : Paris

Description Sujet choisi par Anes MEKKI  
L’extraction de données est un problème récurrent qui a été étudié de différentes
manières. Une approche moderne consiste à définir ce que l’on souhaite
extraire en utilisant des expressions régulières étendues appelées spanners. C’est
en particulier le cas du projet SystemT d’IBM, qui a motivé de nombreux travaux
de recherche en théorie de bases de données [JACM2015], [PODS2014]. Les
spanners sont également utilisés pour l’extraction d’information dans les fichiers
CSV, qui est le format le plus utilisé pour représenter des données tabulaires
[VLDB2016] Cependant, si ces approches déclaratives facilitent la description
des règles d’extraction, leur évaluation demeure complexe, notamment car le
nombre de réponses est susceptible d’être très grand.

Pour remédier à cela, une approche récente consiste à construire une représentation
compacte en mémoire des occurrences du motif sur le texte d’entrée,
puis à les énumérer une par une à partir de cette structure. Cette approche,
appelée énumération, a été très étudiée ces dernières années pour différents
types de données, en particulier pour l’extraction d’information à l’aide de
spanners [PODS2018a], [PODS2018b], mais également dans le cadre classique
des requêtes sur les mots exprimée en logique monadique du second ordre
[PODS2018c].

Hélas, ces travaux actuels ne permettent guère d’évaluer efficacement des
motifs en pratique, car ils nécessitent de traduire les spanners vers des
automates déterministes, ce qui engendre une explosion combinatoire. L’objectif de
ce projet est de concevoir des algorithmes permettant une implémentation
efficace de ces techniques pour l’extraction de données dans un texte. Pour cela,
nous adapterons les méthodes développées pour énumérer les solutions de
circuits proposées dans [ICALP2017] [ICDT2019] [ARXIV2018].

Dans un deuxième temps, nous nous intéresserons à comment on peut main-
tenir à jour la représentation compacte des réponses lorsque le texte d’entrée
est modifiée. Ce problème a été étudié en particulier dans [PODS2018c]. Notre
approche est là encore de proposer des algorithmes implémentables et passant
à l’échelle.

Accéder au sujet détaillé


SL308-41 A predictive tool based on artificial neural networks (ANN) for sinkhole formations  
Encadrement  
Encadrant : Antoine WAUTIER(écrire)
Labo/Organisme : IRSTEA, UR RECOVER
Ville : Aix-en-Provence

Description Sujet choisi par Mathias MICHEL  
Dans le cadre du projet PERCIVAL en collaboration avec le BRGM et le BAM institute de Berlin, un code de calcul aux éléments discrets à été développé afin de simuler l'effondrement de cavités sous-terraines. Plusieurs régimes d'effondrement ont été identifiés mais à ce stade les paramètres d'influence n'ont pas été identifiés.

Dans ce projet, il est proposé d'utiliser les réseaux de neurones artificiels afin d'inférer les paramètres micromécaniques ayant une incidence sur le régime d'effondrement. Un réseau simplifié sera alors construit avec un nombre plus limité de paramètres d'entrée.

Dans un deuxième temps il est envisagé de tester les capacités prédictives du réseau sur des exemples à des échelles plus larges (simulations numériques et données terrain). Ce sera l'occasion de tester la représentativité des simulations numériques aux petites échelles (quelques milliers de grains) pour modéliser des phénomènes aux larges échelles (plusieurs milliards de grains).

Un descriptif plus détaillé est à télécharger.

Accéder au sujet détaillé

Remarques:
Bonjour,

J'ai eu connaissance de l'appel à stage de L3 pour l'ENS de Lyon via la liste de diffusion calcul du CNRS. Le projet de recherche proposé met l'accent sur la compréhension des phénomènes physiques, mais les aspects numériques et algorithmiques restent assez centraux.

Si le sujet vous semble tout de même ne pas coller suffisamment au profil des élèves, pensez vous qu'il puisse intéresser d'autres filières de l'ENS ?

Merci d'avance
Cordialement
Antoine Wautier


SL308-97 Étude de la connexité temporelle et des spanneurs temporels dans les réseaux dynamiques  
Encadrement  
Encadrant : Arnaud CASTEIGTS(écrire)
Labo/Organisme : LaBRI
Ville : Talence

Description Sujet choisi par Valentin PASQUALE  
Le contexte général de ce sujet se situe dans le domaine des réseaux fortement dynamiques, comme par exemple des réseaux de drones, robots, ou véhicules. On peut représenter ces réseaux par des graphes dynamiques (aussi appelés graphes temporels) dans lesquels l’ensemble de sommets (entités) est fixe mais l’ensemble d’arêtes change
au cours du temps. Dans de tels graphes, il devient parfois difficile de résoudre des problèmes algorithmiques habituellement simples dans les graphes statiques.
Un exemple de problème simple dans les graphes classiques qui devient complexe (au sens intellectuel) dans les graphes dynamiques est celui de trouver un ensemble minimum d’arête qui connecte l’ensemble des sommets du graphes. Dans le cas statique, il suffit de sélectionner n’importe quel arbre couvrant, ces derniers ayant tous n − 1 arêtes, où n est le nombre de sommets du graphe. Dans le cas dynamique, où les arêtes ont des temps de présence donnés, il s’agit de sélectionner un ensemble d’arêtes assurant la connexité temporelle du graphe, à savoir qu’un chemin ayant des dates croissantes existe entre
chaque paire de sommets.
Il a récemment été montré que des graphes dynamiques ayant \Theta(n^2) arêtes exis-
tent dans lesquels aucune arête ne peut être enlevée sans compromettre la connexité
temporelle. Ce résultat est surprenant et marque une différence fondamentale entre les graphes dynamiques et les graphes statiques. De façon complémentaire, nous avons montré que tout graphe dynamique basé sur un graphe complet admet un sous-ensemble de O(n log n) arêtes suffisant à assurer la connexité temporelle. Il y a donc un résultat négatif et un résultat positif, mais avec beaucoup de questions ouvertes entre les deux.
Dans ce stage, il s’agira d’abord de se familiariser avec la littérature et les notions
principales sur les graphes dynamiques, et notamment la notion de connexité temporelle. Puis, nous pourrons considérer quelques uns des questions ouvertes et tenter d’y répondre. Que l’on y arrive ou pas, cette activité fera progresser la compréhension actuelle de ces nouveaux objets théoriques, qui sont par ailleurs d’actualité.

Accéder au sujet détaillé

Remarques:
L'hébergement sera pris en charge.


SL308-87 Calcul moléculaire  
Encadrement  
Encadrant : Pierre-Étienne MEUNIER(écrire)
Labo/Organisme : Hamilton Institute, Maynooth University
Ville : Maynooth (Irlande)

Description Sujet choisi par Coline PETIT-JEAN  
Le calcul moléculaire vise à calculer avec des molécules. Il s'agit à la fois d'une recherche à visée fondamentale ("qu'est-ce que la matière autour de nous peut bien être en train de calculer ?"), et appliquée ("comment utiliser la matière pour calculer ?").

Ce domaine combine aussi des approches théoriques et expérimentales, souvent par les mêmes personnes. Les principaux modèles théoriques utilisés sont basés sur des idées de pavages et de calcul asynchrone. Expérimentalement, des biomolécules (ADN, ARN, protéines) sont un bon "langage de programmation moléculaire" pour implémenter nos algorithmes théoriques. On peut citer l'Origami ADN, qui permet de construire des molécules quasiment sur mesure, comme exemple de succès de ce modèle.

Les objectifs de ce stage sont de travailler sur des modèles d'assemblage et/ou de pliage moléculaire pour comprendre comment embarquer du calcul de manière robuste et déterministe dans ce type de processus. Même si notre équipe est surtout intéressée par l'informatique fondamentale, nous avons notre propre labo de chimie pour implémenter nos constructions.


Ce stage se déroulera à Maynooth, près de Dublin, en Irlande. Il n'est pas nécessaire d'avoir une quelconque expérience de biologie ou chimie pour candidater. En revanche, l'esprit de ce sujet est très proche des petits systèmes de calcul (machines de Turing, automates cellulaires, tag systems…), à la fois sur l'aspect théorique et sur l'aspect pratique: avec seulement 4 instructions, il est honnête de reconnaître que l'ADN n'est pas un langage de très haut niveau.


Remarques:
Nous pouvons accueillir plusieurs stagiaires, qui travailleront sur des problèmatiques différentes à définir précisément.

Une aide financière pour le logement (un sujet sensible en Irlande en ce moment) est envisageable.


SL308-95 Méthodes de tree-search en optimisation combinatoire  
Encadrement  
Encadrant : Vincent JOST(écrire)
Labo/Organisme : GSCOP
Ville : grenoble

Description Sujet choisi par Paul REVENANT  
Dans différents champs d'expertise (surtout planning, mais aussi programmation par contraintes), les méthodes de tree-search sont bien maîtrisées.

En optimisation combinatoire et recherche opérationnelle, le transfert de connaissance depuis ces domaines experts n'a pas été complètement accompli.

Le stage aura pour objectif de tester des méthodes de tree-search sur des problèmes combinatoire relativement épurés (des généralisation du voyageur de commerce), afin d'en évaluer la performance.

En particulier, on pourra regarder chercher le plus long cycle/chemin élémentaire dans le graphe définit par les N premier entiers et dans lequel deux entiers sont adjacents si l'un est multiple de l'autre.

Remarques:
Le stage sera encadré par Luc Libralesso, mon doctorant qui travaille sur ces méthodes et vient de gagner le challenge ROADEF 2018 en utilisant une recherche arborescente.


SL308-7 Reversible Causal Graph Dynamics  
Encadrement  
Encadrant : Pablo ARRIGHI(écrire)
Labo/Organisme : LIS UMR 7020
Ville : Marseille

Description Sujet choisi par Mathis ROCTON  
Cellular Automata consist in a grid of identical cells, each of which may take a state among a
finite set. The state of each cell at time t + 1 is computed by applying a fixed local rule to the
state of cell at time t, and that of its neighbours, synchronously and homogeneously across space.
Causal Graph Dynamics extend Cellular Automata from fixed grids, to time-varying graphs.
That is, the whole graph evolves in discrete time steps, and this global evolution is required to
have a number of physics-like symmetries: shift-invariance (it acts everywhere the same), causality (information has a bounded speed of propagation). One could also demand reversibility (the whole evolution is a bijection over the set of labelled graphs). That way we obtain a Computer Science-inspired toy model, that has features mimicking both Quantum theory (reversibility) and General Relativity (evolving topology).

Accéder au sujet détaillé

Remarques:
Possibilité d'indémnisation.


SL308-6 Manhattan InhomogeneousWalk over directed graphs  
Encadrement  
Encadrant : Giuseppe DI MOLFETTA(écrire)
Labo/Organisme : LIS, AMU
Ville : Marseille

Description Sujet choisi par Mathieu ROGET  
During this internship, we will study a discrete-time random walk over a directed graph. Two kind of
graphs will be investigated: the L-lattice, a square lattice on which each step must be perpendicular to is predecessor) and
the Manhattan lattice, in which adjacent rows (columns) have antiparallel directions, corresponding to the trafic pattern in
Manhattan. After a detailed bibliography research, the student will study first the probability for a given graph path, by standard combinatorial methods and then he will realize a numerical simulator. This part of the stage will be not ”original”, but it will be
pedagogically important for the student.
The second and the key part of the internship will demand at the student to introduce a new walker with a non homogeneous
coin. In other words, at each point of the directed graph the probability to go towards the left/right or towards the nord/south of
the graph will depend on the point itself. This will introduce a supplementary metrics in the dynamics which will couple with
the defined topology of the graph. At this point the student will write the finite difference equations governing the walker and
he will have the choice for studying the dynamics by different method: the first may be the standard continuous limit in which
discrete time and space converge to a continuum surface; the second could be space-grouping nodes in macro-nodes by means
of coarse-graining maps in order to investigate the emergent macroscopic behaviour. Moreover the student may complete his
studies building a numerical simulator and study all regimes.

Accéder au sujet détaillé


SL308-61 Comparaison de techniques d'orientation d'axiomes  
Encadrement  
Encadrant : Guillaume BUREL(écrire)
Labo/Organisme : LSV
Ville : Cachan

Description Sujet choisi par Guillaume ROUSSEAU  
Les démonstrations sont rarement recherchées en logique pure mais dans des théories : arithmétique, théorie des ensembles en mathématique ; arithmétique et théories associées aux structures de données en vérification de programmes. Néanmoins, les prouveurs automatiques ont du mal à traiter efficacement ces théories si elles sont présentées comme des axiomes. La démonstration modulo théorie est un cadre qui permet d'outrepasser ceci en présentant les théories comme du calcul, plus précisément comme un système de réécriture. En présentant à la main certaines théories comme un système de réécriture, on a pu montrer que la déduction modulo théorie améliore effectivement la recherche de preuve. Reste la question de savoir comment transformer automatiquement en système de réécriture une théorie présentée au départ comme un ensemble d'axiomes.

Il existe plusieurs techniques pour cela. Certaines sont complètes, dans le sens où elles préservent la prouvabilité par rapport à la théorie de départ. D'autres sont de simples heuristiques basées sur la forme des axiomes. L'objectif de ce stage est de comparer ces différentes techniques en utilisant trois prouveurs automatiques qui implémentent la déduction modulo théorie, à savoir iProverModulo, Zipperposition et ArchSAT. Le stagiaire pourra également être amené à proposer lui-même de nouvelles techniques d'orientation.


Accéder au sujet détaillé

Remarques:
Le LSV ferme à partir du 1er août inclus.


SL308-12 Modèle formel pour la blockchain  
Encadrement  
Encadrant : Thomas GENET(écrire)
Labo/Organisme : IRISA
Ville : Rennes

Description Sujet choisi par Justine SAUVAGE  
Mots clés : Blockchain, méthodes formelles, assistants à la
preuve, algorithmes de consensus distribué, sémantique de langages de
programmation, sécurité.

Lieu : Laboratoire IRISA à Rennes, co-encadrement entre les
équipes CIDRE (sécurité, blockchain, algorithmes de consensus) et CELTIQUE
(méthodes formelles, sémantique des langages de programmation)

Résumé :
La blockchain, au coeur de la cryptomonnaie Bitcoin, est une technique
permettant de construire un registre d'informations partagé et infalsifiable.
Contrairement à ce qui était pratiqué avant Bitcoin, le contrôle
de ce registre n'est pas confié à une entité de confiance mais distribué
entre à tous ses usagers. Dans Bitcoin, les informations stockées dans
ce registre sont simplement des transferts d'argent d'un compte
virtuel à un autre. La sécurité de l'ensemble repose sur l'utilisation
de signatures cryptographiques et d'algorithmes de consensus distribué
garantissant que les pages de ce registre de transferts ne peuvent
être falsifiées par un agent malveillant.

Par dessus la blockchain, de nouveaux protocoles ont vu le jour et
vont au delà des simples transferts monétaires prévus dans
Bitcoin. Dans ces protocoles spécifiques, une large part de la logique
du protocole est programmable par l'utilisateur lui-même. On parle
alors de protocoles de "smart contracts" (comme Ethereum et Tezos) et
de langage de programmation de contrats (Solidity pour Ethereum et
Liquidity pour Tezos). Le fait que ces protocoles soient
programmables par les utilisateurs multiplie les vecteurs d'attaques et
rend leur preuve de sécurité encore plus complexe que dans le cas de
Bitcoin.

Avec les équipes CIDRE et CELTIQUE, nous souhaitons construire un
modèle formel simple et concis du noyau d'un protocole de smart
contract afin d'étudier et de prouver des propriétés de sécurité sur
celui-ci.

Objectifs du stage : l'objectif est de comprendre comment interagissent
les composants clés des protocoles de smart contracts (les algorithmes
de consensus, les primitives cryptographiques, les langages de
contrats, etc.) et à quel niveau se placer pour les formaliser de
façon pertinente par rapport aux propriétés ciblées: propriétés de
consensus, propriétés de sûreté, propriétés de sécurité. Le modèle
formel devra être aisément manipulable dans un assistant à la preuve. Un
des objectifs est donc de produire une formalisation (Coq
ou Isabelle/HOL) du coeur d'un protocole de smart contracts comme
Ethereum ou Tezos. Cette formalisation devra être suffisamment fine
pour permettre de raisonner sur les propriétés de consensus, de sûreté
et de sécurité des contrats et suffisamment générale pour pouvoir être
étendue à d'autres protocoles de smart contracts.

Accéder au sujet détaillé

Remarques:
Co-encadrement par Emmanuelle Anceaume et Thomas Genet. Rémunération prévue.


SL308-33 Pgcd rapide et reconstruction de fraction rationnelle  
Encadrement  
Encadrant : Romain LEBRETON(écrire)
Labo/Organisme : LIRMM
Ville : Montpellier

Description Sujet choisi par Amin SIDI-ALI-CHERIF  
Ce stage propose de faire de l’algèbre effective, un mélange d’informatique et de mathématique qui vise à faire des calculs d’algèbre efficacement sur ordinateur.
Pour calculer le pgcd de deux polynômes, l’approche historique est l’algorithme d’Euclide. Ce procédé répète des divisions euclidiennes pour que les degrés des restes baissent jusqu’à obtenir un reste nul. Nous souhaitons nous intéresser à l’approche opposée qui utilise des divisions euclidiennes par les degrés faibles. Ainsi les valuations des restes augmentent plutôt que leur degrés baissent. Les deux approches disposent d’algorithmes rapides de type diviser pour régner [GG13, Chapitre 11], [GJV03]. Le premier objectif de ce stage est de comprendre le lien entre les deux approches et de voir si la
deuxième approche n’aboutirait pas à un algorithme plus rapide.
L’une des applications du pgcd est la reconstruction rationnelle [BCG + 17, Chapitre 7.1]. Pour des raisons d’efficacité, il est commun d’éviter de faire des calculs directement sur des fractions rationnelles, et de les remplacer par leur développements limités, c’est-à-dire des polynômes modulo x^d . Il faut alors être capable de retrouver la fraction rationnelle à partir de son développement limité : c’est le problème de la reconstruction rationnelle.
Le deuxième objectif de ce stage est d’utiliser le pgcd par les degrés faibles pour reconstruire la fraction rationnelle au fur et à mesure que l’on calcule son développement limité. Ceci est d’autant plus important que l’on ne connait pas a priori la précision d nécessaire. L’algorithme que l’on propose de créer permettra de détecter immédiatement et sans calculs superflus cette précision d nécessaire.
Tous les algorithmes de ce stage devront être codés sur SageMath. En effet, le stage est centré sur des améliorations pratiques. Cette implémentation nous donnera une première idée des performances et sera aussi utile pour la bonne compréhension du sujet.


Accéder au sujet détaillé

Remarques:
Co-encadrement avec Pascal Giorgi http://www.lirmm.fr/~giorgi/
Possibilité de rémunération


SL308-8 Localisation d’une cible invisible cachée dans un graphe  
Encadrement  
Encadrant : Nicolas NISSE(écrire)
Labo/Organisme : I3S/INRIA
Ville : Sophia-Antipolis

Description Sujet choisi par Emile SORCI  
cf. pdf joint.

Accéder au sujet détaillé

Remarques:
Co-encadrement avec Julien Bensmail (MCF, Université Côte d'Azur).


SL308-90 Featured network embedding using GCN Variational Autoencoders  
Encadrement  
Encadrant : Márton KARSAI(écrire)
Labo/Organisme : ENS Lyon / LIP / IXXI
Ville : Lyon

Description Sujet choisi par Eliot TRON  
The creation of links in a complex network is largely determined by the entangled effects of nodes’s similarities in terms of their individual characters and their network position. However, feature and structural characters of nodes usually appear to be correlated making it difficult to determine, which of them is more responsible for the formation of the emergent network structure. The aim of this internship would be to further develop a node embedding methods, which ultimately aims at disentangling the information shared by the structure of a network and the features of its nodes. Building on the recent developments of Graph Convolutional Networks (GCN), the method relies on multitask GCN Variational Autoencoders where different dimensions of the generated embeddings can be dedicated to encoding feature information, network structure, and shared feature-network information. The task of the candidate would be to explore possible improvement of the actual method by developing new architectures based on the actual learning scheme.

Remarques:
The internship will employ a single candidate - L3 student coming from the fields of Computer Science. The candidate should present programming skills and basic understanding of graph theory and statistical learning, with an interest in complex networks and data-driven research. The internship will be carried out at ENS Lyon-LIP in the DANTE Inria team, and will take place at IXXI Rhone-Alpes Complex System Institute under the supervision of Márton Karsai and instructions of Sébastien Lerique.


SL308-9 Calcul de couplages contraints dans les graphes  
Encadrement  
Encadrant : Nicolas NISSE(écrire)
Labo/Organisme : I3S/INRIA
Ville : Sophia-Antipolis

Description Sujet choisi par Zoe VARIN  
cf. pdf joint.

Accéder au sujet détaillé

Remarques:
Co-encadrement avec Julien Bensmail (MCF, Université Côte d'Azur).


SL308-94 Algorithmes pour le problème de sac à dos disjonctif  
Encadrement  
Encadrant : François CLAUTIAUX(écrire)
Labo/Organisme : Inria Bordeaux Sud-Ouest
Ville : Talence

Description Sujet choisi par Nina VESSERON  
Le stage concerne la conception d'algorithmes pour résoudre un problème d'optimisation combinatoire : le sac à dos disjonctif.

Programme de travail :
- lecture d'articles décrivant les algorithmes qui vont composer la méthode à implémenter
- implémentation de la méthode de résolution
- validation expérimentale
- rapport décrivant les algorithmes et les expérimentations


Cf. description détaillée jointe.

Accéder au sujet détaillé

Remarques:
Co-encadrement Pierre Pesneau (Institut de Mathématiques de Bordeaux)

Le stagiaire sera accueilli au sein de l'Institut de Mathématiques de Bordeaux



Eric Thierry

Valid HTML 4.01 Transitional