SM207-1 Attack-defense trees for computer security  
Admin  
Encadrant : Barbara KORDY
Labo/Organisme : IRISA
URL : http://people.irisa.fr/Barbara.Kordy/internships.php
Ville : Rennes

Description  

An attack-defense tree (ADTree) is an AND-OR tree representing how an attacker may compromise a system and how a defender can protect it against potential attacks. Nodes of ADTrees are labeled with (collections of) actions that the attacker and the defender need to perform in order to reach their goals. ADTrees extend the industrially recognized model of attack trees with nodes representing countermeasures. ADTrees may also assist the security analysts in the process of quantitative evaluation of security scenarios, by integrating algorithms to estimate parameters such as the cost, the impact or the probability of a successful attack.

With the help of ADTrees, one can express how to protect a system against potential attacks. In practice, however, preventive countermeasures may not be fully effective and may be difficult or expensive to deploy. This is why, in some situations, the attacks are not prevented in advance and instead defensive countermeasures are used once an attack occurs. Security training is an example of a preventive countermeasure; blocking a credit card after its theft illustrates a reactive countermeasure. A practical an industrially pertinent formal tool for security evaluation and risk assessment must therefore be able to differentiate between preventions and reactions.

The objective of this master project is to increase the expressive power of ADTrees by integrating reactive countermeasures into the model.

The objective of the project will be reached by addressing the following two research goals:
1. Develop mathematical foundations for ADTrees with preventive and reactive countermeasures.
2. Propose quantitative evaluation techniques for ADTrees with preventive and reactive countermeasures.

The extended model of ADTrees with preventions and reactions will be validated in a real-life case study. The case study will be performed with one of our industrial partners specialized in risk assessment and consulting. The underlying goal is to verify the usability of the proposed formalization as well as to test the efficiency and the scalability of the developed algorithms.
URL sujet détaillé : people.irisa.fr/Barbara.Kordy/internships/master_internship_ADTrees.pdf :

Remarques : le stage sera rémunéré



SM207-2 AUTOMATIC MINIMIZATION OF LARGE SYSTEMS OF EQUATIONS  
Admin  
Encadrant : Tribastone MIRCO
Labo/Organisme : IMT School for Advanced Studies
URL : sysma.imtlucca.it :
Ville : Lucca (Italy)

Description  

A significant hindrance to our capability of modeling many natural and engineered systems is the challenge in solving large systems of equations. This has led to a number of approaches aimed at taming complexity by means of abstraction and simplification techniques, developed across many disciplines such as control theory, ecology, economics, informatics, and systems biology.

The subject of this internship proposal is to progress a recent line of investigation on the automatic reduction of systems of ordinary differential equations using techniques grounded in foundational theories of computer science, such as behavioral equivalences and partition refinement algorithms.

Currently available results concern exact notions of minimization, where from a reduced model one can precisely recover the dynamics of the original system. Starting from this, we propose three possible future directions of work, also motivated by specific real-world applications in machine learning, systems biology, and electrical networks:

- The development of novel exact notions of minimization to capture still uncovered aggregation patterns.

- The development of approximate variants where larger reductions are possible at the expense of introducing a (hopefully controllable) error in the reduced model.

- The development of equivalence relations checked through statistical sampling, to help overcome computational difficulties in particularly challenging real-world systems.

The work will be carried out at IMT School for Advanced Studies Lucca, one of Italy's six schools of excellence for post-graduate education. As the research is part of an ongoing collaboration with Microsoft Research Cambridge and the University of Oxford, interested candidates might also have the opportunity of stays at these institutions in order to develop part of their project. Publication in high-profile CS venues can be expected as an output of this work.
URL sujet détaillé : :

Remarques :



SM207-3 Vérification de systèmes distribués communiquant par messages  
Admin  
Encadrant : Aurélie HURAULT
Labo/Organisme : IRIT
URL : https://www.irit.fr/-Equipe-ACADIE-
Ville : Toulouse

Description  

Complex distributed applications are built by composing distributed services/processes/peers. These peers asynchronously interact with messages. As there exist many asynchronous communication models (with various guarantees on delivery order, faults etc) corresponding to the diversity of deployment platforms, the correctness of the composition is not trivial. Ideally, this correctness is formally and automatically verified: formalization is required to ensure confidence in the case of critical systems; automation is needed to facilitate changes.

Our team have developed a framework based on TLA+ (transition systems) to verify the asynchronous composition of services. Several communication models are available and generic results to compare these models have been discovered and proved. This framework is currently limited to a fixed number of peers without dynamic creation of peers or of communication channels. A demo can be played with at http://vacs.enseeiht.fr/.

The objectives are:
- to discover the framework and to extend it to allow the description of parameterized systems; this also requires to extend the peer description language (currently CCS; pi-calculus may be a solution);
- to extend the framework so that messages and transitions carry applicative values;
- to extend the framework to allow dynamic creation of peers, of communication channels, and their exchange.
The three objectives require both theoretical work (to identify the relevant abstractions), formalization (to describe them in TLA+) and development (to integrate them in the framework).

URL sujet détaillé : http://hurault.perso.enseeiht.fr/sujet-master-ens-2016.pdf

Remarques : Co-encadrement : Philippe Quéinnec (queinnec.fr)



SM207-4 Termination checking in Dedukti  
Admin  
Encadrant : Frédéric BLANQUI
Labo/Organisme : LSV
URL : http://rewriting.gforge.inria.fr/
Ville : Cachan

Description  

Dedukti is a formal proof checker based on a logical framework called the
λΠ-calculus modulo, which is an extension of the simply-typed lambda-calculus
with dependent types and an equivalence relation on
types generated by the user-defined rewrite rules. Proofs generated by some
automated theorem provers or proof assistants can be checked in Dedukti by encoding function definitions and
axioms by rewrite rules. But, for Dedukti to behave well, the rewrite rules
must satisfy some properties like confluence, preservation of typing and termination.
The goal of this internship is to develop a termination checker for Dedukti.
Such a termination checker could later be extended to other languages like Coq,
Agda or Haskell, and participate to the international competition of termination
provers.
URL sujet détaillé : http://rewriting.gforge.inria.fr/divers/termin.pdf

Remarques :



SM207-5 Proof tactics in Dedukti  
Admin  
Encadrant : Frédéric BLANQUI
Labo/Organisme : LSV
URL : http://rewriting.gforge.inria.fr/
Ville : Cachan

Description  

Dedukti is a formal proof checker based on a logical framework called the λΠ-calculus modulo, which is an extension of the simply-typed lambda-calculus with dependent types and an equivalence relation on types generated
by user-defined rewrite rules. Proofs generated by some automated theorem
provers or proof assistants can
be checked in Dedukti by encoding function definitions and axioms by rewrite
rules.
But, currently, no proof assistant fully uses all the features of Dedukti, which
allows arbitrary user-defined rewrite rules (e.g. (x + y) + z → x + (y + z), where
+ is itself defined by other rules). Such rules are indeed necessary if one wants
to ease the use of dependent types and, for instance, be able to define types for
representing simplicial sets of arbitrary dimensions, ∞-categories or models of
Voevodsky's homotopy type theory.
The goal of this internship is to develop a set of basic tactics for trying to
solve Dedukti subgoals automatically, or help develop Dedukti proofs interac-
tively.
URL sujet détaillé : http://rewriting.gforge.inria.fr/divers/tactics.pdf

Remarques :



SM207-6 Refinement in Dedukti  
Admin  
Encadrant : Frédéric BLANQUI
Labo/Organisme : LSV
URL : http://rewriting.gforge.inria.fr/
Ville : Cachan

Description  

Dedukti is a formal proof checker based on a logical framework called the λΠ-calculus modulo, which is an extension of the simply-typed lambda-calculus with dependent types and an equivalence relation on types generated by user-defined rewrite rules. Proofs generated by some automated theorem provers or proof assistants can
be checked in Dedukti by encoding function definitions and axioms by rewrite
rules.
But, currently, no proof assistant fully uses all the features of Dedukti, which
allows arbitrary user-defined rewrite rules.
We therefore would like to develop a tool for interactively building Dedukti
proofs using all the features of Dedukti. But, to scale up and be able to handle
large developments, especially with dependent and polymorphic types, we need
to allow the users to write down incomplete terms (e.g. the type of the elements
of a list), and provide an inference engine for finding out the missing subterms.
The goal of this internship is then to develop such a refinement engine for
Dedukti.
URL sujet détaillé : http://rewriting.gforge.inria.fr/divers/unif.pdf

Remarques :



SM207-7 Interactive proofs with Dedukti  
Admin  
Encadrant : Frédéric BLANQUI
Labo/Organisme : LSV
URL : http://rewriting.gforge.inria.fr/
Ville : Cachan

Description  

Dedukti is a formal proof checker based on a logical framework called the λΠ-calculus modulo, which is an extension of the simply-typed lambda-calculus with dependent types and an equivalence relation on types generated by the user-defined rewrite rules. Proofs generated by some
automated theorem provers or proof assistants can be checked in Dedukti by encoding function definitions and axioms by rewrite rules.
But, currently, no proof assistant fully uses all the features of Dedukti, which
allows arbitrary user-defined rewrite rules.
The goal of this internship is to develop an interface for Dedukti, that is, a
tool for enabling users to build Dedukti proofs interactively.
URL sujet détaillé : http://rewriting.gforge.inria.fr/divers/interface.pdf

Remarques :



SM207-8 A parallel Branch-and-bound algorithm for asymetric p-median problems  
Admin  
Encadrant : Pascal REBREYEND
Labo/Organisme : H=F6gskolan Dalarna / Microdata-analyse department
URL : http://www.du.se/en/Research/Research-Profiles/Complex-Systems-Microdata-Analysis/
Ville : Borlange / Suède

Description  

The topic of this internship is to design and develop a parallel branch and bound method for such problem. This includes design of heuristics to compute lower-bound. The design of a branch and bound will be done in a specific context due to problems adressed: The number of candidate points to locate on is much more smaller than the set of demand points. Typically, for a full country like Sweden, we have p which is between 10 and 200 while the number of candidates points is around 2000. We can also use geographical information to design lower bound heuristics. Parallel (multi-threading and message passing methods) are also planed.

The student will work in C, in a Linux environment. Good knowledge of algorithms and data-structure is recommended, as well as previous experiences of multi-threading and parallel programming.
URL sujet détaillé : http://users.du.se/~prb/Stage/ENS_2017.pdf

Remarques : - Pas de possibilité de rémunération
- H=F6gskolan Dalarna finance chaque année 3 à 4 doctorants dans le profil de recherche microdata analyse.



SM207-9 Efficient and modular higher-order rewriting  
Admin  
Encadrant : Frédéric BLANQUI
Labo/Organisme : LSV
URL : http://rewriting.gforge.inria.fr/
Ville : Cachan

Description  

Dedukti is a universal proof checker developed at INRIA in Deducteam. It has been designed so as to be small but powerful enough to express and check formal proofs coming from various automated theorem provers and interactive proof assistants. It is like a logical framework with the additional advantage of preserving computations by allowing shallow embeddings. The current Dedukti library contains hundreds of Mo of proofs, hence efficiency is important.
Bindlib is an OCaml library developed at the University of Chambéry providing efficient data
structures for manipulating terms with bound variables, used in the programming language PML.
Some preliminary experience shows that a re-implementation of Dedukti based on Bindlib could be faster, simpler and easier to extend.
The main objective of this internship will be to develop and test a new implementation of Dedukti based on Bindlib.
URL sujet détaillé : http://rewriting.gforge.inria.fr/divers/bindlib.pdf

Remarques : Co-advising by Olivier Hermant (Mines ParisTech). One or two weeks will be spent in Chambéry with the developers of Bindlib.



SM207-10 Locally irregular decompositions of graphs  
Admin  
Encadrant : Julien BENSMAIL
Labo/Organisme : I3S
URL : https://team.inria.fr/coati/
Ville : Sophia-Antipolis

Description  

A locally irregular decomposition of an undirected graph G, is a partition E1,...,Ek of E(G), such that each Ei induces a graph where every two adjacent vertices have distinct degrees. Locally irregular decompositions were recently introduced as a tool to deal with particular cases of the well-known 1-2-3 Conjecture. They may as well be considered as a measure of how far from irregular a graph is.

As a main conjecture on locally irregular decompositions, it was addressed whether every graph admitting locally irregular decompositions, can be decomposed into at most 3 locally irregular graphs. At the moment, we are still far from a full proof of that conjecture. To support that conjecture, it was verified for several classes of decomposable graphs, including most complete graphs and trees, and graphs with large minimum degree. In the context of decomposable bipartite graphs, it was recently shown that decompositions into at most 9 locally irregular graphs always exist. Using that result, it was shown that every decomposable graph can be decomposed into at most 328 locally irregular graphs. This confirms that a constant number of locally irregular graphs are sufficient to decompose any decomposable graph.

Several directions may be considered during this internship:

1. Prove the conjecture above for new classes of graphs.
2. Improve the proofs of 9 and 328, to get better bounds in both the bipartite and general contexts.
3. Imagine and develop new decomposition approach to improve these bounds further down.

Please have a look to the attached URL, for more details.
URL sujet détaillé : http://www-sop.inria.fr/members/Julien.Bensmail/datas/sujet-locally-irregular.pdf

Remarques :



SM207-11 Virtualization boundary for optimized cloud-delivered security  
Admin  
Encadrant : Sylvie LANIEPCE
Labo/Organisme : Orange Labs
URL : http://www.orange.com/fr/accueil
Ville : CAEN

Description  

In cloud virtualized platform, the primary role of virtualization layer is to present carefully isolated and elastic virtual resource quantities to multiple tenant software stacks, with two dominant approaches the hardware-level virtualization and more recently the OS-level virtualization (container).
Some research works propose to rethink what is called the virtualization boundary that is, find an optimal boundary between the virtualizing part and the virtualized domains [1, 2]. Other works are in favor of revisiting OSes to optimize their execution on virtualized platform [3, 4, 5]. Finally, promising introspection technics - a concept to monitor Virtual Machines from the hypervisor level in order to inspect states and activities of Operating Systems running Inside them =96 are highly dependent on the capacity of the virtualization layer to interpret virtualized domains activities [6].
This project has the objective to find out potential benefits on a security point of view of reconsidering the virtualization boundary, with two main aspects: better infrastructure security and enabling security services based on the virtualization layer to be delivered to the tenants (while benefiting from isolation, high privileges and a cross-view of VMs at that layer).

References
[1] Van Moolenbroek, David C., Raja Appuswamy, and Andrew S. Tanenbaum. "Towards a flexible, lightweight virtualization alternative" In Proceedings of International Conference on Systems and Storage (SYSTOR '14), ACM, 2014
[2] Dan Williams and Ricardo Koller, =91Unikernel Monitors: Extending Minimalism Outside of the Box', USENIX Workshop on Hot Topics in Cloud Computing (HotCloud'16}, Denver, US, June 2016
[3] Nikos Vasilakis, Ben Karel and Jonathan M. Smith, =93From Lone Dwarfs to Giant Superclusters: Rethinking Operating System Abstractions for the Cloud=94 , 15th Workshop on Hot Topics in Operating Systems (HotOS XV), Usenix, May 2015
[4] Kivity, Avi, Dor Laor, Glauber Costa, Pekka Enberg, Nadav Har'El, Don Marti, and Vlad Zolotarov. "OSv=97optimizing the operating system for virtual machines" In usenix annual technical conference (Usenix ATC 14), 2014
[5] MADHAVAPEDDY, A., MORTIER, R., ROTSOS, C., SCOTT, D.,SINGH, B., GAZAGNAIRE, T., SMITH, S., HAND, S., and CROWCROFT, J. =91Unikernels: Library operating systems for the cloud' In Proc. of ACM ASPLOS, Houston, TX, Mar. 2013
[6] Bauman, Erick and Ayoade, Gbadebo and Lin, Zhiqiang, A Survey on Hypervisor-Based Monitoring: Approaches, Applications, and Evolutions, ACM Comput. Surv., volume 48- 1, September 2015


In this project, the intern will conduct a preliminary study of this research topic by making an extensive state of the art, in the aim of identifying =96 as part of future research - potential optimizations in virtualization boundary abstractions targeting virtualized platform security and low layers monitoring capabilities for delivering virtualization-based security services.
The internship will contribute to a more precise understanding of the topic, from a cloud infrastructure provider point of view (impacts and opportunities), and can lead to a publication and/or a PhD on the topic.


Requisite skills and abilities:
Strong inclination to Research in low layers computing (operating system, virtualization and to some extends hardware architectures)
Security
Habits in reading research papers
Excellent analytical capabilities
Motivated by industrial research

URL sujet détaillé : :

Remarques :



SM207-12 Analog continuous time machines and models of computation  
Admin  
Encadrant : Olivier BOURNEZ
Labo/Organisme : LIX, Ecole Polytechnique
URL : https://www.lix.polytechnique.fr/
Ville : Palaiseau

Description  


General Presentation

Today's theoretical computer science, and in particular classical computability and complexity is dealing with computations over a discrete space with a discrete space. This aims at modeling today's computers, which are digital computers working over bits. This covers today's machines, and today's classical models such as Turing machines working over words over a finite alphabet with a discrete time.
But machines where time is continuous can be considered and can indeed be built. Such machines are analog, and are working over continuous quantities like voltage. Notice that first ever built program- mable computers where actually analog machines. This includes for example the differential analysers that were first mechanical machines working over quantities encoded by angles of shafts, and later on electronic machines working over quantities like continuous voltages. Such machines were typically used to solve ordinary differential equations. Realizing today analog computer does not yield to major dif- ficulties : see example http://images.math.cnrs.fr/Lorenz-Rossler-ampli-op-et-calcul-analogique.html for a nice introduction (in French), or [8] for a book about the history of computing, not forgetting analog computing history as in most of the books.
It turns out that the corresponding computability and complexity theory has not received so much attention : even if models of computation where space could be continuous and time remains discrete have been considered (see e.g. [1], or [9]), these models are still discrete time. Notice that there is no hope to get a unification of the type of Church-Turing thesis for such models.
The purpose of this internship is to focus on continuous time and space models : i.e. truly analog models of computation such as differential analysers or electronic analog computers. In this context, some very recent results seem to show that some unification of models is indeed possible, and that there might be something similar in spirit to Church Turing thesis, for many aspects, including computability, complexity, logic, proof theory, and machines.

Context of the work

Some recent results prove that there indeed exists a nice computability and complexity theory for continuous time and space models, with strong equivalence results : The General Purpose Analog Computer (GPAC) of Claude Shannon [7] is the first historical model of a continuous time programmable computer. Shannon proposed this as a model of Differential Analysers on which he was acting as a operator. Daniel Grac ̧a and Felix Costa proved in [5] that functions that can be generated by a GPAC correspond to functions solutions of an ordinary differential equation with polynomial right-hand side.
How it compares to Turing machines ? We proved in [2] with some coauthors that the model can actually compute all functions computable by a Turing machines : i.e. that analog models have the same computational power than Turing machines. All of this is about computability.
But an important issue is also complexity : could such analog machines compute some functions faster than modern digital machines ?
Very recently, Amaury Pouly proved in his PhD [6] that it is not, and more importantly that it is indeed possible to talk about time complexity in such analog models (solving a famous known open problem). The obtained complexity turns out to be equivalent to classical complexity : polynomial time (the class P of the famous P = NP ? question) corresponds to computations by trajectories of polynomial length.
As a proof of recognition of the interest of such a result, let us mention that this result received the best paper award at the conference ICALP this summer (track B) [4].
With other coauthors, we also proposed recently a formalization of algorithms covering discrete and continuous time machines. This result received the best paper award at the conference CIE this summer [3].
These results are only first steps and open many ways to original and unexpected understanding of many classical concepts and questions.
For example, of possibly also explaining other classes like NP, the P = NP question as simple questions about ordinary differential equations, or about understanding better fundamental questions like the understanding of what a machine is, a model is, or a proof is in the general case, that is to say even when talking about the continuum. Notice that it relates not only to computer science questions, but also to mathematical and even philosophical aspects about these questions.

Description of the work

The objective of this internship is to contribute to understanding and developing the theory of complexity for analog models.
Many variations of the precise intended work for the duration of the internship are possible ac- cording to the preferences of the candidate. This could involve complexity, logic, machine aspects, or optimization related issues. We have preliminary ideas for all the following questions.
As an example, one objective could be to look if one can indeed go further than talking only about polynomial time : can we characterize similarly non-deterministic computations (NP) or polynomial space (P SP ACE) ? How to measure space and non-determinism for analog models ? etc. . .
As another example, one objective could be to better understand how continuous time algorithms can be formalized. In particular, what are the associated proof techniques ? How far can we go in the formalization in the spirit of [3] ? Can we relax our axiomatization of time ?
As a third example, one objective could be to apply these results to practical questions of optimi- zations or verification. Can we derive more efficient algorithms in related contexts ? Can we present some algorithms in a new way using this framework ?

R ́ef ́erences

[1] L. Blum, M. Shub, and S. Smale. On a theory of computation and complexity over the real numbers ; NP completeness, recursive functions and universal machines. Bulletin of the American Mathematical Society, 21(1) :1=9646, July 1989.
[2] Olivier Bournez, Manuel L. Campagnolo, Daniel S. Grac ̧a, and Emmanuel Hainry. Polynomial differential equations compute all real computable functions on computable compact intervals. Journal of Complexity, 23(3) :317=96335, June 2007.
[3] Olivier Bournez, Nachum Dershowitz, and Pierre N ́eron. Axiomatizing analog algorithms. In Arnold Beckmann, Laurent Bienvenu, and Natasa Jonoska, editors, Pursuit of the Universal - 12th Conference on Computability in Europe, CiE 2016, Paris, France, June 27 - July 1, 2016, Proceedings, volume 9709 of Lecture Notes in Computer Science, pages 215=96224. Springer, 2016.
[4] Olivier Bournez, Daniel S. Gra ̧ca, and Amaury Pouly. Polynomial Time corresponds to Solutions of Polynomial Ordinary Differential Equations of Polynomial Length. The General Purpose Analog Computer and Computable Analysis are two efficiently equivalent models of computations. In ICALP 2016, volume 55 of LIPIcs, pages 109 :1=96109 :15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
[5] Daniel S. Grac ̧a and Jos ́e F ́elix Costa. Analog computers and recursive functions over the reals. Journal of Complexity, 19(5) :644=96664, 2003.
[6] Amaury Pouly. Continuous models of computation : from computability to complexity. PhD thesis, Ecole Polytechnique and Unidersidade Do Algarve, Defended on July 6, 2015. 2015. https ://pastel.archives-ouvertes.fr/tel-01223284.
[7] C. E. Shannon. Mathematical theory of the differential analyser. Journal of Mathematics and Physics MIT, 20 :337=96354, 1941.
[8] Bernd Ulmann. Analog computing. Walter de Gruyter, 2013.
[9] K. Weihrauch. Computable Analysis : an Introduction. Springer, 2000.
URL sujet détaillé : http://www.lix.polytechnique.fr/~bournez/uploads/Main/sujet-2016-17-1.pdf

Remarques : There is no specific prerequisite for this internship. The formation of ENS Lyon is perfect for this internship.



SM207-13 Interactive structure and appearance optimization for shape design  
Admin  
Encadrant : Jonàs MART=CDNEZ
Labo/Organisme : INRIA
URL : http://alice.loria.fr/
Ville : Nancy

Description  

Full details of the research subject can be found at https://dl.dropboxusercontent.com/u/3592218/int_struct_app_opt.pdf


Research topic

In structural optimization, the field of topology optimization seeks to optimize shapes under structural objectives, such as achieving the most rigid shape using a given quantity of material and a loading scenario. An interactive algorithm for two dimensional topology optimization has already been proposed [1]. An algorithm is considered to be interactive if the response time is below seconds [3].

Inspired by topology optimization methods, we recently introduced a technique [2] that automatically generates rigid shapes answering a specific loading scenario and resembling an input exemplar pattern, while using a user-specified quantity of material. However, the whole optimization takes up to minutes to converge. Our current goal is to devise an optimization algorithm with faster convergence (interactivity), that will allow the user to explore between changing loading scenarios and exemplar pattern parameters. This is specially interesting for artists and designers, being able to interactively adjust the aesthetic and functional (rigidity) specifications optimization variables. In this regard, we could collaborate together with the École d'art de Nancy.

The main challenges arising are:
- Structural analysis performance. The current main bottleneck of computation. Among others, reduced order methods to compute the elastic compliance could be explored.
- Optimization formulation. The original optimization proposed in is infeasible for interactivity. An alternative formulation could be devised.
- Optimization convergence. We are facing a highly non-linear optimization problem. The interactive changes of the optimization parameters (e.g. the boundary conditions) impose additional difficulties that need to be carefully studied.

In addition, the method could be extended to optimize for several interleaved 3D planes.

The master student will tackle the aforementioned problems in a multidisciplinary team at INRIA Nancy, that is currently working in the intersection between computer graphics and structural optimization.
In addition to devising efficient optimization algorithms, the student will be expected to 3D print the results of the optimization, in order to verify their expected mechanical properties.


Requisites

* Strong programming skills (C++, Python and OpenCL).
* Knowledge of structural optimization and finite element methods will be appreciated.
* Highly proficient in spoken and written English.


References

1] Aage, N., Nobel-J=F8rgensen, M., Andreasen, C. S., and Sigmund, O. Interactive topology optimization on hand-held devices. Structural and Multidisciplinary Optimization 47, 1 (2013), 1=966.
[2] Mart=EDnez, J., Dumas, J., Lefebvre, S., and Wei, L.-Y. Structure and appearance optimization for controllable shape design. ACM Trans. Graph. 34, 6 (Oct. 2015), 229:1=96229:11.
[3] Miller, R. B. Response time in man-computer conversational transactions. In Proceedings of the December 9-11, 1968, Fall Joint Computer Conference, Part I (1968), pp. 267=96277.

URL sujet détaillé : https://dl.dropboxusercontent.com/u/3592218/int_struct_app_opt.pdf

Remarques :



SM207-14 Optimal motion planning for FDM 3D printers  
Admin  
Encadrant : Haichuan SONG
Labo/Organisme :
URL : http://alice.loria.fr/
Ville : Nancy

Description  

Optimal motion planning for FDM 3D printers

Keywords: 3D printing, motion planning
Advisors: Haichuan Song, Sylvain Lefebvre (http://www.antexel.com/sylefeb/)
Email: haichuan.song.fr, sylvain.lefebvre.fr
Center: INRIA Nancy - Grand Est (http://www.inria.fr/centre/nancy)
Team: ALICE project-team (http://alice.loria.fr/)

1. Research topic
3D printing recently became widely available, as the cost of printers and materials has been driven down by the maker movement and FabLabs. This was accompanied by open source software efforts to provide users with tools to prepare instructions for printers and to control the printer motion from these instructions (firmware). Interestingly, this also revealed some open questions regarding how to best perform these tasks, and a renewed interest in the research community for the related geometric and algorithmic problems. Our team has recently contributed several novel algorithms to help modeling and prepare parts for 3D printing [1,2,3,4]. We are now investigating issues which are closely related to the 3D printing process and in particular the motion of the printing device, with a focus on filament printers (but similar problems are found across different technologies).

Filament 3D printers manufacture an object by depositing melted plastic in layers, from bottom to top. Models are manufactured by moving the nozzle, which deposits filament, along precomputed printing paths. After finishing printing one path, the extruder moves to the next (this is called a travel move as no material is deposited).

Provided that P0 and T0 are the position and speed at the end of last printing path, P1 and T1 are the desired position and speed at the start of next printing path. The motion from P0 to P1 and is unknown - a key question is to determine its optimal parameters - knowing that the end motion is performed by a discrete mechanical device (stepper motors).

While we seek to minimize travel time, the moving speed varies significantly with the curve shape as the acceleration is restricted by mechanical limitations. Other constraints can also be considered, for example the collision with existing prints should be avoided [3].

The overall goal of this research is to consider optimal motion planning for 3D printing, given the geometry of the printing paths. The order, start/end points and travel moves are free variables. We will focus on several aspects:
- Designing travel motion curves with theoretically optimal motion speed.
- Specifying the instructions for stepper motors that will give the maximum speed along the curves.
- Optimizing globally for start/end points along cyclic print paths to accelerate the entire process.
This will reduce the total printing time for filament 3D printers, and has both great theoretical and practical values. This internship will include three phases:
- Survey on previous work in related areas, for example: CNC path planning, CAD, additive manufacturing, motion planning in robotics.
- Derivation of theoretical equations and formula.
- Implementation and embedding in IceSL [4] and experimental printer firmware.
We will print and measure results on a range of 3D printers available in the lab.

2. Requisites
- Strong programming skills (C++ and/or Python).
- Strong basis in Mathematics, especially in geometry.
- Willingness to confront theory to practical implementations.
- Highly proficient in spoken and written English.


References
[1] T. Reiner, N. Carr, R. Mech, O. St'ava, C. Dachsbacher, and G. Miller, "Dual-color mixing for fused deposition modeling printers," in Computer Graphics Forum, vol. 33, pp. 479-486, Wiley Online Library, 2014.
[2] H.-C. Song, N. Ray, D. Sokolov, and S. Lefebvre, "Anti-aliasing for fused filament deposition," arXiv preprint arXiv:1609.03032, 2016.
[3] J. Hergel and S. Lefebvre, "Clean color: Improving multi-filament 3d prints," in Computer Graphics Forum, vol. 33, pp. 469-478, Wiley Online Library, 2014.
[4] http://www.loria.fr/~slefebvr/icesl/.



URL sujet détaillé : https://www.dropbox.com/s/fpd5csxtcaw1mvo/Optimal_motion_planning_for_FDM_3D_printers.pdf?dl=0

Remarques :



SM207-15 A New paradigm for Data Management in Cloud environment  
Admin  
Encadrant : Eddy CARON
Labo/Organisme : LIP
URL : http://avalon.ens-lyon.fr
Ville : Lyon

Description  

A fundamental characteristic of our era is the deluge of data. Data is everywhere from scientific applications, e-business, information, social network, etc. This leads to a situation where each community develops specialized data manager tailored for the needs of their applications. Through this training we plan to explore a new paradigm that allows for generic, flexible and autonomous data management. In this approach, data can behave autonomously and interact with their environment according to their own data management requirements and policies. We plan to develop a distributed and autonomous environment where the data is controlled by itself, enabling a smart behavior. We plan to start with a set of basic services implementing reliable storage, security and privacy, and efficient file transfer. Later, we will explore services composition in order to provide more advanced features such as quality of service and green data management. This M2 training will be the basement of this ambitious project.

URL sujet détaillé : :

Remarques : Christian Perez should participate to this training if the software component sounds as a good approach.



SM207-16 Contraintes sur des domaines paramétriques  
Admin  
Encadrant : Charlotte TRUCHET
Labo/Organisme : LINA - UMR 6241 - Université de Nantes
URL : http://www.normalesup.org/~truchet/
Ville : Nantes

Description  

Constraint Programming aims at modeling and solving combinatorial problems, in a declarative way. The problem is modeled with variables (unknowns), each taking a value in a given domain, and constraints, predicates on the variables. Each constraint comes with its own partial solving method (its propagator), used in the solvers to efficiently search for solutions. In the classical CP framework, domains are a rather poor structure: finite integer intervals, or finite sets. In previous work, we extended the definition of a CP domain in the same way as abstract domains in abstract interpretation, with much richer domains representations. The goal of this internship is to study a new extension where the domains can be parametric, with variable bounds for instance. This extension would be very useful in many problems, for instance verification of parametrized programs. A possible roadmap is: first, study the CLP(FD) logical framework which expresses propagators as rules, and extend it to parametric domains. This may need steps of symbolic computations (over the domains bounds). Second, define an abstract domain with these rules propagators, and add a choice operator on this domain. Finally, implement the domain in the AbSolute solver (a constraint solver over abstract domains, in OCaml).


URL sujet détaillé : http://www.normalesup.org/~truchet/Docs/master2017.pdf

Remarques : The internship can be funded, by an ANR project (Coverif) if necessary. It can be extended to a PhD grant on the same project.
David Cachera (Celtique team, IRISA, Rennes), will be co-advisor.




SM207-17 6 mois  
Admin  
Encadrant : Anca MOLNOS
Labo/Organisme : CEA Leti
URL : http://www.leti.fr/
Ville : Grenoble

Description  

Today many available processor architectures give the opportunity to extend their Instruction Set Architecture (ISA) with specialised units to accelerate highly-demanded functions, such us, machine learning, data mining, cryptography. In the embedded systems domain, the RISC-V, a free and open RISC ISA from Berkeley University (https://riscv.org/), is a notable example in this direction. This open ISA initiative gains a lot of momentum, and has many industrial and academic contributors
providing core implementation and tools, such as, LLVM compiler, hardware simulator.

In this context, the proposed internship addresses the open issue of how to compile high-level C code to generate highly-efficient instructions for a specialised accelerator.
For this work, the targeted accelerators are functional units with adequate arithmetic precision, stemming from the cutting-edge research area of approximate computing.
Adequate or approximate computing is a paradigm in which the calculations are executed in adequate rather than maximum precision, in order to accelerate the execution or save power [1]. The internshit is in link with the ANR project ARTEFaCT (http://artefact.insa-rennes.fr/).
The student's tasks are:
- Familiarise with the current RISC-V simulator and extend it with few adequate-precision operation/kernels, such as, multiplication, division, convolution, required in the hot workloads mentioned above. These operations are already available in CEA. Estimated work effort: 1 month.
- Get acquainted with the existing RISC-V compilation chain and augment it with code generation support for the extension operations. Estimated work effort: 3 months.
- Exercise and optimise the code generation for several applications from AxBench, an approximate computing benchmark (http://axbench.org/). Analyse and compare the performance results with existing methods. Estimated work effort: 2 months.
- Document and present the work. This activity will take place during the entire duration of the project, with increased focus towards the last internship month.

The preferred candidate should have an expertise in software architecture and compilers, and a background in processor architecture concepts. She/he should be at ease with classical software programming environments, e.g., Python, C/C++, and should be highly motivated to work in a multi-disciplinary environment such as the one in CEA.

The student will be guided to perform high-quality research and developement in several crucial aspects for an embedded systems expert, covering software and hardware, and touching upon the integration of software in widely-utilised open source processor and tools.
Moreover, we aim for publication in an international workshop or conference, when the results are of sufficient quality.

To apply, please send your CV at: anca dot molnos at cea dot fr
URL sujet détaillé : :

Remarques : The internship will be remunerated.



SM207-18 Runtime System for efficient executions on heterogeneous architectures  
Admin  
Encadrant : Abdoulaye GAMATIÉ
Labo/Organisme : LIRMM - CNRS
URL : http://www.lirmm.fr/~gamatie
Ville : Montpellier

Description  

** Keywords:
OpenMP programming models, OpenMP 4.0, Compilation techniques, LLVM, Runtime, Multicore Architectures


** Description:
State-of-the-art energy-efficient multicore embedded systems adopt in major part heterogeneous architectures combining CPUs with compute accelerators such as GPUs. The ARM big.LITTLE technology (e.g., adopted in the Samsung Exynos 5422 chip) rather promotes a single-ISA heterogeneous and adaptive architecture paradigm according to which a runtime can dynamically migrate application workloads between two different clusters of ARM cores: a low-power cluster (referred to as =93LITTLE=94) and a high performance cluster (referred to as =93big=94). All these cores communicate via a cache coherent interconnect, which consists of a bus.

This internship addresses the definition of adequate mapping and migration policies that provide the best energy-efficiency for such single-ISA heterogeneous architectures. Here, the considered application workloads to be executed are assumed to be programmed in OpenMP 4.0. One possible approach is to adapting the corresponding runtime of OpenMP and the LLVM compiler so as to take into account both the task/thread execution monitoring and the best allocation to available cores so as to obtain a good compromise in terms of performance and energy consumption. The expected solution will be validated on a real board providing an ARM single-ISA heterogeneous platform, the Odroid XU4.
URL sujet détaillé : :

Remarques : This internship will be co-advised with Dr. Gilles Sassatelli. This position will be funded.



SM207-19 Exploiting Non-Volatile Memories for Aggressive Energy Reduction in Embedded Systems  
Admin  
Encadrant : Abdoulaye GAMATIÉ
Labo/Organisme : LIRMM - CNRS
URL : http://www.lirmm.fr/~gamatie
Ville : Montpellier

Description  

** Keywords:
Non-Volatile Memories, STT-MRAM, Memory Hierarchy, Magnetic Logic, Cache Memory Architectures, Compiler Analysis, Energy-Efficiency, Embedded Systems


** Description:
Major issues encountered in integrated circuits for advanced technology node include high leakage current, performance saturation and increased device variability. For battery-powered embedded systems, energy consumption is a high critical metric. The energy consumed by memory activities is generally not negligible in the overall system energy cost. The memory architecture design should be therefore carefully considered in connection with data management across the different levels of memory hierarchy. Non-volatile memories (NVMs) such as Magnetic RAM have very attractive properties in that they can be the golden solution to address challenge. Thanks to their non-volatility, NVMs have zero leakage power.

This internship aims at building an energy-proportional memory architecture system model that is capable of adapting the non volatile feature of considered memories with data storage requirements in the memory, depending on the executed workloads. These requirements could be identified via static or dynamic analysis performed by a compiler. Spin Transfer Torque (STT) RAMs are considered as target NVMs in the current study due to their maturity and presence in consumer electronics. There are already several existing simulation and energy/latency estimation tools for NVMs, such as NVSim or CACTI that could serve for investigating the problem during this internship.
URL sujet détaillé : :

Remarques : This internship will be co-advised with Prof. Lionel Torres. This position will be funded.



SM207-20 Learning Techniques for Performance and Energy Prediction in Adaptive Manycore Systems  
Admin  
Encadrant : Abdoulaye GAMATIÉ
Labo/Organisme : LIRMM - CNRS
URL : http://www.lirmm.fr/~gamatie
Ville : Montpellier

Description  

** Keywords:
Machine Learning, Data-Mining, Multicore Architectures, Prediction model, Runtime management, Performance and Energy Monitors, Adaptive Resource Allocation


** Description:
The growing demand for smarter high-performance embedded systems leads to the integration of multiple functionalities in on-chip systems with tens (even hundreds) of cores. In the same time, the low energy consumption requirement of such manycore systems has to be preserved. This opens a number of design challenges among which it is worth mentioning the optimal resource allocation that is necessary to reach the best compromise on performance and energy consumption.

This internship aims at investigating the applicability of recent learning approaches in order to help for a more efficient resource allocation in manycore systems. Given a set of information monitored from a manycore platform, prediction models could be built so as to forecast relevant metrics, e.g., execution time, power consumption. These information could be collected from system executions performed with either cycle accurate simulators or real multicore compute boards. The predicted metrics are therefore exploited for adapting the resource allocation to workload requirements in terms of performance and power tradeoff.
URL sujet détaillé : :

Remarques : This internship will be co-advised with Dr. Gilles Sassatelli. This position will be funded.



SM207-21 Reasoning on Dynamic Attributed Graphs  
Admin  
Encadrant : Rachid ECHAHED
Labo/Organisme : LIG lab (Laboratoire d'Informatique de Grenoble)
URL : http://lig-membres.imag.fr/echahed/
Ville : Grenoble

Description  


keywords: Program verification, Graph transformation, Dynamic logics, Hoare calculi

The objective of this project is to tackle the problem of correctness
of programs processing graphs and graph-like structures annotated with
data. Graph-like structures are used almost everywhere when
representing or modelling structures and systems, not only in applied
and theoretical computer science, but also in, e.g., natural and
engineering sciences.

Analysis, correctness verification and bug finding in programs with
unbounded memory (graph) size require decidable and efficient logics.
Development of logics appropriate for the task is challenging due to
the delicate balance between high expressivity and low complexity. On
the one hand, appropriate logics must be able to express the semantic
properties of the memory. On the other hand, the complexity of
reasoning tasks in the logics must be low enough to permit practical
use. Real-world programs very often have memory which is unbounded in
size. When programs in traditional imperative programming languages
need to deal with an unbounded number of data items, they implement
dynamic data structures such as lists and trees to store their
data. However, programming with dynamic data structures is complex and
error-prone. Verifying the correctness of such programs is a
notoriously hard area of computer-aided verification.

In a recent work [1,2], a rule-based programming language, which
handles memories of unbounded size without resorting to dynamic data
structures, has been introduced together with some decidable logics to
capture completely the effects of programs in this programming
language. The methods of [1,2] model the memory as a graph (pointer
structure) lacking any data (where data means here values or
attributes belonging to datatypes such as integers or strings). This
focus on graph structures ignoring data was prudent as an initial
approach, since the analysis of pointer structures is in itself very
challenging already without data. As such, the programming language of
[1,2] does not allow datatypes or any datatype-specific operation
(e.g. arithmetic or string concatenation). However, real-world
programs use the memory to store data which they manipulate.

The goal of this project is to develop a framework extending that of
[1,2] which supports datatypes and operations on data as well as a
formalism for analyzing programs. A Hoare-like calculus will be
developed for the considered programs based on some specific classical
or dynamic logics.

For more details please contact the supervisor at: echahed.fr
This project could be followed by a 3 years PhD thesis in the
considered area. Other projects related to graph transformations are
available.


Work plan.

1. Get familiar with graph transformation techniques as well as some
of the intended proof techniques (small dedicated bibliography).

2. Extend procedures in [2] in order to take into account
attributes(data), startig with decidable theories (e.g.
Presburger arithmetic, strings).

3. Design and implement a first prototype if time permits

[1] J. Brenas, R. Echahed and M. Strecker:
Proving Correctness of Logically Decorated Graph Rewriting
Systems. FSCD 2016: 14:1-14:15

[2] J. Brenas, R. Echahed and M. Strecker:
Ensuring Correctness of Model Transformations while Remaining
Decidable. ICTAC 2016: to appear.



URL sujet détaillé : :

Remarques : This project could be followed by a 3 years PhD thesis.

Paid internship



SM207-22 Attaques par canaux auxiliaires sur les schémas post-quantiques  
Admin  
Encadrant : Thomas PREST
Labo/Organisme : LCH (Thales)
URL : https://www.di.ens.fr/~prest/
Ville : Gennevilliers

Description  

Les récents progrès vers la construction d'ordinateurs quantiques remettent en cause la sécurité des protocoles cryptographiques classiques. En effet, ceux-ci sont basés sur les problèmes de la factorisation et du logarithme discret, que de tels ordinateurs pourraient aisément résoudre. La cryptographie post-quantique utilise d'autres objets mathématiques sur lesquels ils existe des problèmes supposés difficiles pour les ordinateurs quantiques: les réseaux euclidiens, les codes correcteurs, les fonctions de hachage, les polynômes multivariés, etc.

D'autre part, les attaques par canaux auxiliaires permettent d'exploiter des données physiques (temps d'exécution, consommation électrique, etc.) mesurables durant l'exécution d'un algorithme pour en extraire les éléments secrets. Ces attaques ont donné les meilleurs résultats pratiques connus et sont un domaine extrêmement actif de la recherche appliquée.

L'organisme de standardisation NIST a lancé un appel à candidatures pour standardiser des schémas post-quantiques. Dans ce contexte, la résistance aux attaques par canaux auxiliaires sera un critère discriminant. L'arrivée récente d'implémentations pratiques de schémas post-quantiques a permis l'étude et la réalisation d'attaques par canaux auxiliaires qui donnent déjà d'excellents résultats.

L'objectif de ce stage est d'étudier la vulnérabilité aux attaques par canaux auxiliaires de schémas post-quantiques. Dans un premier temps, un état de l'art des schémas résistant aux attaques quantiques sera effectué. Puis le stagiaire étudiera la vulnérabilité aux attaques par canaux auxiliaires d'un schéma préalablement choisi. Enfin, il pourra proposer des contre-mesures aux attaques mises en valeur. Les résultats obtenus pourront faire l'objet d'une publication académique.
URL sujet détaillé : https://www.di.ens.fr/~prest/Stages/Stages_LCH_2017.pdf

Remarques : Plusieurs remarques:
- C'est un stage en entreprise. Il y a deux encadrants, tous deux industriels titulaires d'une thèse
- une rémunération d'environ 1250=80 est proposée
- la durée du stage est d'environ 6 mois
- une thèse après le stage est possible, mais pas systématique
De plus amples précisions sont apportées dans le pdf joint.



SM207-23 Méthode GLV en dimension 4 sur les Q-courbes  
Admin  
Encadrant : Olivier BERNARD
Labo/Organisme : LCH (Thales)
URL : https://www.thalesgroup.com/en/worldwide/defence/news/thales-communications-security
Ville : Gennevilliers

Description  

La cryptographie à base de courbes elliptiques demeure actuellement un outil incontournable permettant d'apporter efficacement de hauts niveaux de sécurité aux applications civiles et militaires. Les courbes standardisées par le NIST dans la norme FIPS 186-2 ont maintenant plus de 15 années, et récemment les révélations d'Edward Snowden ont levé des doutes quant au fait que ces courbes puissent cacher des vulnérabilités.

Dans ce contexte, le besoin d'une nouvelle génération de courbes elliptiques, telle qu'initiée par le NIST en 2015 (Workshop on Elliptic Curve Cryptography Standards), sert deux motivations~: la première est de retrouver la confiance du public, la seconde est de bénéficier des multiples avancées algorithmiques de la dernière décennie.

Ces avancées permettent, notamment via le choix de nouveaux modèles de courbes et de lois d'addition complètes, d'obtenir de meilleures performances hardware et software, des implémentations plus simples et plus sûres, des propriétés de résistance aux timing attacks ou aux side-channel attacks.

La courbe FourQ proposée par Microsoft Research semble adresser à la fois les problématiques de performances, de simplicité et de sécurité. Elle concurrence directement la courbe Curve25519 de Bernstein.

Basée sur les familles de Q-courbes de Smith, elle combine l'utilisation des endomorphismes de Frobenius et de la multiplication complexe, la loi d'addition fortement unifiée des modèles d'Edwards tordus, le tout modulo un nombre premier de la forme 2^n - epsilon.

Le but de ce stage est de reproduire les gains de performances obtenus par Costello et Longa, ainsi que, si le temps le permet, de proposer des améliorations et des extensions à des niveaux de sécurité plus élevés.
URL sujet détaillé : https://www.di.ens.fr/~prest/Stages/Stages_LCH_2017.pdf

Remarques : Plusieurs remarques:
- C'est un stage en entreprise. Il y a deux encadrants
- une rémunération d'environ 1250=80 est proposée
- la durée du stage est d'environ 6 mois
- une thèse après le stage est possible, mais pas systématique
De plus amples précisions sont apportées dans le pdf joint.



SM207-24 Sécurisation du Cloud - Schémas de recherche sur données chiffrées avancés  
Admin  
Encadrant : Alexandre ANZALA YAMAJAKO
Labo/Organisme : LCH (Thales)
URL : https://www.thalesgroup.com/en/worldwide/defence/news/thales-communications-security
Ville : Gennevilliers

Description  

La constante augmentation des débits de connexion et l'apparition sur le marché d'appareils mobiles aux ressources plus limitées que celles d'un ordinateur personnel, engendrent de nouveaux besoins. Après la démocratisation des services de messagerie électronique, l'avènement du cloud computing offre de nouvelles perspectives aux utilisateurs comme le partage de médias (documents, musique, vidéos, livres) et d'applications (tableurs, traitement de texte, affichage de documents, requêtes à des bases de données).

La récente impulsion du projet Cloudwatt visant à doter la France d'une infrastructure de cloud souveraine s'explique notamment par les problématiques de sécurité liées à l'hébergement de données sur un serveur distant qui n'est pas nécessairement de confiance. Cependant, la recherche d'un niveau de service plus élevé via l'adaptation de résultats académiques sur la recherche sur données chiffrées à un contexte opérationnel reste aujourd'hui peu répandue.

Les schémas de chiffrement totalement homomorphique initialement proposés par Gentry, c'est-à-dire les schémas dont la fonction de chiffrement conserve la structure d'anneau, apportent une réponse théorique à la problématique générale de manipulation aveugle de données chiffrées mais imposent encore aujourd'hui des contraintes qui empêchent leur adoption au sein de systèmes opérationnels. En se concentrant sur la problématique plus restreinte de recherche sur les données chiffrées, on se donne alors la possibilité d'obtenir des schémas présentant des garanties de sécurité sans sacrifier l'aspect pratique.

Dans ces schémas un client stocke ses données sur un serveur en dehors de son périmètre de confiance tout en conservant la possibilité d'effectuer des recherches sur ces données. La propriété de sécurité que l'on cherche à atteindre est que le serveur distant opère sans découvrir ni les requêtes ni leurs réponses. Des publications récentes ainsi que des travaux internes ont conduit à valider la possibilité de schémas pratiques de recherche sur données chiffrées. L'objectif est aujourd'hui de consolider et d'apporter des fonctionnalités supplémentaires aux travaux existants

Description du stage
===================En s'appuyant sur des travaux internes, le (la) stagiaire sera amené(e) à réaliser une étude bibliographique des schémas de recherche sur données chiffrées symétriques en portant une attention particulière au schéma de D. Cash et al. introduit à CRYPTO 2013 ainsi que des extensions génériques liées. Sur la base de ces résultats, on évaluera le compromis entre sécurité et fonctionnalités selon trois axes :
- l'ajout du dynamisme (ajout, suppression de fichier) ;
- l'adaptation pour des requêtes évoluées (booléennes, sur des intervalles, sur des sous-chaînes) ;
- l'intégration de capacité de délégation et de révocation de droits de recherche à des tiers.

De solides compétences en cryptographie sont nécessaires, ainsi qu'une bonne maitrise de l'algorithmique. Une certaine aisance en programmation, notamment dans le langage C, sera très appréciée.
URL sujet détaillé : https://www.di.ens.fr/~prest/Stages/Stages_LCH_2017.pdf

Remarques : Plusieurs remarques:
- C'est un stage en entreprise. Il y a deux encadrants
- une rémunération d'environ 1250=80 est proposée
- la durée du stage est d'environ 6 mois
- une thèse après le stage est possible, mais pas systématique
De plus amples précisions sont apportées dans le pdf joint.



SM207-25 Multiple Internship offers for Technicolor R&D France TRD_2017_OFF_001  
Admin  
Encadrant : Laurence PIQUET
Labo/Organisme : Technicolor R&D France
URL : www.technicolor.com :
Ville : CESSON SEVIGNE

Description  

With more than 100 years of experience and innovation, Technicolor is a major actor in entertainment, software, and gaming worldwide. With strong historical ties to the largest Hollywood studios, the company is a leading provider of production, postproduction and distribution for creators and distributors of content. Technicolor is a world leader in film processing, a leading supplier in the field of decoders and gateways and one of the largest manufacturer and provider of DVD & Blu-ray discs. The recent acquisition of The Mill, a leading visual effects and content creation studio for the advertising, gaming and music industries adds one more first-rate brand to our already robust portfolio (MPC, Mikros Image and Mr. X), effectively making Technicolor the leader in VFX and post production services to the advertising production segment
The company also has a strong activity in Intellectual property and Licensing business.
This unique environment presents an exceptional opportunity to explore cutting-edge video technologies that will reach homes in the years to come. In Rennes research and development center, our research engineers will make your internship a fascinating and rewarding experience.
For more information, please visit our website: www.technicolor.com
You can discover all our internship offers on:
http://www.technicolor.com/en/innovation/student-day/

Objectives /misions
Our interns' mission is to help researchers identify new approaches, implement new algorithms, perform tests and benchmarks and contribute to the implementation of demos and prototypes within research teams.
We offer research internship opportunities in multiple fields:
- Computer Graphics (CG)
- Computer Vision (CV),
- Data Mining (DM)
- Human Computer Interaction (HCI)
- Networking (NW)
- Video Processing (VP)
Details of the internships offered within these thematics at http://www.technicolor.com/en/innovation/student-day/job-internship-opportunities-ri-labs
Apply at stage.rennes.com
Monthly allowance: =801200 gross

Profile
- Student in Master 2 in an engineering school or university
- Specialization in one of the fields above
- Inquiring mind, inventive, passionate .
- Skills in prototyping applications on PC or embedded platforms
- Good English level

To apply:
If you are interested in joining us, please visit our web site and consult our internship open positions at http://www.technicolor.com/en/innovation/student-day/job-internship-opportunities-ri-labs
and apply at stage.rennes.com
Group: Technicolor (www.technicolor.com) / Research & Innovation.
Position: Intern -
Location: Rennes, FRANCE -
Deadline: Open.
Compensation: =801200 per month (before taxes)

URL sujet détaillé : http://www.technicolor.com/en/innovation/student-day/job-internship-opportunities-ri-labs

Remarques : Compensation: =801200 per month (before taxes)



SM207-26 Search patterns in string on Xeon Phi/GPU for a Artificial Evolution simulator  
Admin  
Encadrant : Jonathan ROUZAUD-CORNABAS
Labo/Organisme : Inria-Beagle/LIRIS
URL : https://team.inria.fr/beagle/
Ville : VILLEURBANNE

Description  

The purpose of this internship is to adapt algorithms and their optimizations that exist in the field of bioinformatics to the specific needs of the simulation software Aevol(http://www.aevol.fr) we develop in the team.

In practice, we need to find sequences of characters in strings with a rate of acceptable difference between the desired pattern and the found. Unlike the use of these techniques in bioinformatics, not a single DNA (character string) has to be processed once but thousands of DNA sequences and not once but millions of times per simulation execution. The algorithms and their optimization will therefore be different.

In addition to the execution on CPU, this type of algorithm should be able to greatly benefit from GPU see Intel Phi / KNL accelerators. Part of the internship will be to adapt / optimize, port and evaluate the performance and accuracy of the algorithms developed on these different hardware architectures.

Depending of the desires, skills of the student and its curriculum, the internship can be oriented more towards the algorithmic conception and optimization work or to the massively parallel architecture support.

The expanded name for the Beagle research group is "Artificial Evolution and Computational Biology". Our aim is to position our research at the interface between biology and computer science and to contribute new results in biology by modeling biological systems. In other words we are making artifacts - from the Latin artis factum (an entity made by human art rather than by Nature) - and we explore them in order to understand Nature. Our research is based on an interdisciplinary scientic strategy: We are developing computer science formalisms and software for complex system modeling in synergy with multidisciplinary cooperations in the area of living sciences. Thanks to computational approaches we study abstractions of biological systems and processes in order to unravel the organizational principles of cellular systems.

Aevol is an open-source digital genetics platform that captures the evolutionary process using genetic algorithms and individual based modeling. Digital organisms in Aevol reproduce, compete and mutate, evolving for hundreds of thousands of generations under typical Darwinian dynamics. Individuals living in large populations interact both on ecological and evolutionary timescales, allowing us to investigate scenarios typically experimentally unattainable, as we can directly control and vary the characteristics of selection (e.g. population size, type of environment, environmental variations) or variation (e.g. types and rates of mutations and rearrangements, horizontal transfer).


URL sujet détaillé : :

Remarques :



SM207-27 From a shared memory to a distributed and load balanced memory paradigm for an artificial evolution simulator  
Admin  
Encadrant : Jonathan ROUZAUD-CORNABAS
Labo/Organisme : Inria-Beagle/LIRIS
URL : https://team.inria.fr/beagle/
Ville : VILLEURBANNE

Description  

The purpose of this internship is to go from a shared memory paradigm (with parallelism as OpenMP task) for the artificial evolution simulator Aevol (http://www.aevol.fr) to a distributed memory paradigm (MPI).

Beyond the software engineering aspect of porting the code, the underlying problems of dynamically load balance the computing is critical. Indeed, the computational model of the simulator can be formalized as a stencil but the amount of computation at each point in the grid is very heterogeneous. In addition, the biological model, which is implemented should enable several specific optimizations (possibility of formalizing a performance prediction model for each grid point). The course is divided into 2 parts: part more parallelization of the code and algorithmic work on the dynamic allocation of computing, performance models and the efficiency of large-scale simulator.

The expanded name for the Beagle research group is "Artificial Evolution and Computational Biology". Our aim is to position our research at the interface between biology and computer science and to contribute new results in biology by modeling biological systems. In other words we are making artifacts - from the Latin artis factum (an entity made by human art rather than by Nature) - and we explore them in order to understand Nature. Our research is based on an interdisciplinary scientic strategy: We are developing computer science formalisms and software for complex system modeling in synergy with multidisciplinary cooperations in the area of living sciences. Thanks to computational approaches we study abstractions of biological systems and processes in order to unravel the organizational principles of cellular systems.


Aevol is an open-source digital genetics platform that captures the evolutionary process using genetic algorithms and individual based modeling. Digital organisms in Aevol reproduce, compete and mutate, evolving for hundreds of thousands of generations under typical Darwinian dynamics. Individuals living in large populations interact both on ecological and evolutionary timescales, allowing us to investigate scenarios typically experimentally unattainable, as we can directly control and vary the characteristics of selection (e.g. population size, type of environment, environmental variations) or variation (e.g. types and rates of mutations and rearrangements, horizontal transfer).
URL sujet détaillé : :

Remarques :



SM207-28 Differential Equation Solver on GPU/Xeon Phi for an artificial evolution simulator  
Admin  
Encadrant : Jonathan ROUZAUD-CORNABAS
Labo/Organisme : Inria-Beagle/LIRIS
URL : https://team.inria.fr/beagle/
Ville : VILLEURBANNE

Description  

The aim of this internship is to design and/or adapt a differential equation solver library for the specific needs of the simulation software Aevol (http://www.aevol.fr) we develop the team. Compared to parallel existing solvers, where the need is to solve a large system of equations over long time scales, we need to solve thousands of systems on small time scales. In addition to the execution on CPU, solving such particular differential equation should greatly benefit from GPU or Intel Phi / KNL accelerators. Part of the internship will be to adapt/optimize, port and evaluate the performance and accuracy of the proposed solver on these different hardware architectures. Depending of the student desires and skills and his curriculum, the internship can be oriented more towards the algorithmic optimization work or to the massively parallel architecture support.

The expanded name for the Beagle research group is "Artificial Evolution and Computational Biology". Our aim is to position our research at the interface between biology and computer science and to contribute new results in biology by modeling biological systems. In other words we are making artifacts - from the Latin artis factum (an entity made by human art rather than by Nature) - and we explore them in order to understand Nature. Our research is based on an interdisciplinary scientic strategy: We are developing computer science formalisms and software for complex system modeling in synergy with multidisciplinary cooperations in the area of living sciences. Thanks to computational approaches we study abstractions of biological systems and processes in order to unravel the organizational principles of cellular systems. Aevol is an open-source digital genetics platform that captures the evolutionary process using genetic algorithms and individual based modeling. Digital organisms in Aevol reproduce, compete and mutate, evolving for hundreds of thousands of generations under typical Darwinian dynamics. Individuals living in large populations interact both on ecological and evolutionary timescales, allowing us to investigate scenarios typically experimentally unattainable, as we can directly control and vary the characteristics of selection (e.g. population size, type of environment, environmental variations) or variation (e.g. types and rates of mutations and rearrangements, horizontal transfer).
URL sujet détaillé : :

Remarques :



SM207-29 Model repository  
Admin  
Encadrant : Brahim HAMID
Labo/Organisme : IRIT
URL : https://www.irit.fr/~Brahim.Hamid/
Ville : Toulouse

Description  

Repositories of modeling artifacts have recently gained increasing attention for the enforcement of reuse in software engineering[3,4]. Repository-centric development processes are adopted in software/system development, such as architecture- or pattern-centric development processes. The proposed framework for building a reuse repository is based on metamodeling techniques that enable the specification of the repository structure and interfaces on content in the form of modeling artifacts and model transformation techniques for the purpose of generation [1,2]. We begin by specifying a conceptual model of the desired reuse repository and proceed by designing modeling languages that are appropriate for the content. The results of these efforts are used to specify and build the repository. The next step is devoted to populating the repository by defining appropriate modeling artifacts. We have proposed an operational architecture for the implementation of a reuse repository. In addition, the tool suite promotes the separation of concerns during the development process by distinguishing the roles of different stakeholders. Access to the repository is customized regarding the development phases, the stakeholder's domain and his system knowledge. The approach for developing a repository of models is generic; however, the discussion and implementation in the context of our experiment is based on the Eclipse platform, Ecore and a CDO-based repository. We have implemented a prototype named SemcoMDT to support the approach as an Eclipse plug-in.

During the implementation and deployment experience, we encounter several technical problems and limitations due to the CDO-based implementation. We plan to study the usage of other infrastructures to support a reuse model repository and their integration with other MDE tools, primarily the access tool, with regard to the development phases and the stakeholders' domain and system knowledge. Additionally, more sophisticated techniques to derive artifacts relationships can be implemented, possibly using different domains, to reduce the complexity to design systems of modeling artifacts. We seek new technologies combined with modeling. Therefore, we will investigate implementation based on an FCA (Formal Concept Analysis) [5]. Each level of abstraction is structured with a lattice, and each lattice is linked. These lattices provide the architect or developer with intelligible classifications for model features. Thus, they enable the search of a model to be indexed, which verifies certain types of properties at a desired level of abstraction. This approach has three advantages: (1) Usability: possibility to dynamically and easily insert a new model; extracting a model can be simply and rapidly realized; (2) Implementation: the space that is required to implement this structure can be optimized; and (3) Visualization: the obtained lattices can be used not only as a component index to ease a search but also as a way for visualizing the content of a reuse repository using a graphical interface.

Bibliography :

[1] Hamid, B., 2016b. A Model Repository Description Language - MRDL. In: International Conference on Software Reuse (ICSR). Vol. 9679 of LNCS. Springer.

[2] Hamid, B., 2016a. A Model-Driven Approach for Developing a Model Repository: Methodology and Tool Support. Future Generation Computer Systems, Elsevier.

[3] Burégio, V., de Almeida, E., Ludrédio, D., Meira, S., 2008. A Reuse Repository System: From Specification to Deployment. In: Mei, H. (Ed.), High Confidence Software Reuse in Large Systems. Vol. 5030 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, pp. 88=9699.

[4] France, R. B., Bieman, J. M., Cheng, B. H. C., 2006. Repository for Model Driven Development (ReMoDD). In: MoDELS Workshops'06. pp. 311=96317.

[5] Ganter, B., Stumme, G., Wille, R., 2005. Formal Concept Analysis. Foundations and Applications. Springer.


To apply, please send your CV at: hamid at irit dot fr


URL sujet détaillé : :

Remarques : The internship will be remunerated. It can be extended to a PhD grant on the same project.



SM207-30 Model repository  
Admin  
Encadrant : Brahim HAMID
Labo/Organisme : IRIT
URL : https://www.irit.fr/~Brahim.Hamid/
Ville : Toulouse

Description  

Repositories of modeling artifacts have recently gained increasing attention for the enforcement of reuse in software engineering[3,4]. Repository-centric development processes are adopted in software/system development, such as architecture- or pattern-centric development processes. The proposed framework for building a reuse repository is based on metamodeling techniques that enable the specification of the repository structure and interfaces on content in the form of modeling artifacts and model transformation techniques for the purpose of generation [1,2]. We begin by specifying a conceptual model of the desired reuse repository and proceed by designing modeling languages that are appropriate for the content. The results of these efforts are used to specify and build the repository. The next step is devoted to populating the repository by defining appropriate modeling artifacts. We have proposed an operational architecture for the implementation of a reuse repository. In addition, the tool suite promotes the separation of concerns during the development process by distinguishing the roles of different stakeholders. Access to the repository is customized regarding the development phases, the stakeholder's domain and his system knowledge. The approach for developing a repository of models is generic; however, the discussion and implementation in the context of our experiment is based on the Eclipse platform, Ecore and a CDO-based repository. We have implemented a prototype named SemcoMDT to support the approach as an Eclipse plug-in.

During the implementation and deployment experience, we encounter several technical problems and limitations due to the CDO-based implementation. We plan to study the usage of other infrastructures to support a reuse model repository and their integration with other MDE tools, primarily the access tool, with regard to the development phases and the stakeholders' domain and system knowledge. Additionally, more sophisticated techniques to derive artifacts relationships can be implemented, possibly using different domains, to reduce the complexity to design systems of modeling artifacts. We seek new technologies combined with modeling. Therefore, we will investigate implementation based on an FCA (Formal Concept Analysis) [5]. Each level of abstraction is structured with a lattice, and each lattice is linked. These lattices provide the architect or developer with intelligible classifications for model features. Thus, they enable the search of a model to be indexed, which verifies certain types of properties at a desired level of abstraction. This approach has three advantages: (1) Usability: possibility to dynamically and easily insert a new model; extracting a model can be simply and rapidly realized; (2) Implementation: the space that is required to implement this structure can be optimized; and (3) Visualization: the obtained lattices can be used not only as a component index to ease a search but also as a way for visualizing the content of a reuse repository using a graphical interface.

Bibliography :

[1] Hamid, B., 2016b. A Model Repository Description Language - MRDL. In: International Conference on Software Reuse (ICSR). Vol. 9679 of LNCS. Springer.

[2] Hamid, B., 2016a. A Model-Driven Approach for Developing a Model Repository: Methodology and Tool Support. Future Generation Computer Systems, Elsevier.

[3] Burégio, V., de Almeida, E., Ludrédio, D., Meira, S., 2008. A Reuse Repository System: From Specification to Deployment. In: Mei, H. (Ed.), High Confidence Software Reuse in Large Systems. Vol. 5030 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, pp. 88=9699.

[4] France, R. B., Bieman, J. M., Cheng, B. H. C., 2006. Repository for Model Driven Development (ReMoDD). In: MoDELS Workshops'06. pp. 311=96317.

[5] Ganter, B., Stumme, G., Wille, R., 2005. Formal Concept Analysis. Foundations and Applications. Springer.


To apply, please send your CV at: hamid at irit dot fr


URL sujet détaillé : :

Remarques : The internship will be remunerated. It can be extended to a PhD grant on the same project.



SM207-31 Interplay of security and software architecture  
Admin  
Encadrant : Brahim HAMID
Labo/Organisme : IRIT
URL : https://www.irit.fr/~Brahim.Hamid/
Ville : Toulouse

Description  

In a recent paper [1], we proposed pattern and properties specification languages to support the pattern-based development of secure software systems. Providing clear, precise, correct and implementable pattern specification is not enough for using a pattern in an automatic way in software engineering development processes. Patterns usually are used in the form of collections of patterns. The pattern of each system and the interaction of patterns within each system are usually well captured and managed. The problem is unpredictable interactions between pattern systems or even between individual patterns. Every system has its particular set of patterns and a much bigger set of unspecified pattern interaction potentials and therefore pattern interaction errors. The interplay between requirements engineering and architecting has been well established but we lack methods and tools to support it. There has been a renewed interest in how to support the Twin Peaks model [2] in a wide range of aspects, such as theoretical frameworks for relating requirements and architecture, tools and techniques such as goal-oriented inference and uncertainty management, problem frames and service composition. There are also approaches for applying the Twin Peaks model in the context of security [3]. There has also been a discussion of the similarities between the problem and solution space and the way
of interpreting requirements and design decisions based on the viewpoint of a stakeholder [4].

The goal of this work is to improve this research by investigating more concepts and more semantics to define a new formal modeling paradigm for compositional security within a pattern-based approach as a foundation for novel security engineering practices. We will use concepts such as tactics [5], which have been applied for architectural patterns but not yet to architecture/security composition and integration.


Bibliography :

[1] Hamid, B., G=FCrgens, S., Fuchs, A., 2016. Security patterns modeling and formalization for pattern-based development of secure software systems. Innovations in Systems and Software Engineering, Springer 12 (2), 109=96140.

[2] Avgeriou, P., Grundy, J., Hall, J. G., Lago, P., Mistr=EDk, I. (Eds.), 2011. Relating Software Requirements and Architectures. Springer.

[3] Heyman, T., Yskout, K., Scandariato, R., Schmidt, H., Yu, Y., 2011. The security twin peaks. Proceedings of the International Symposium on Engineering Secure Software and Systems (ESSoS). Vol. LNCS 6542 of Lecture Notes in Computer Science. Springer, pp. 167=96180.

[4] Schmidt, H., J=FCrjens, J., 2011. Connecting Security Requirements Analysis and Secure Design Using Patterns and UMLsec. In: 23rd International Conference on Advanced Information Systems Engineering (CAiSE). Vol. 6741 of LNCS. Springer, pp. 367=96382.

[5] Bass, L., Clements, P., Kazman, R., 2013. Software Architecture in Practice (3rd Edition). Addison Wesley.



To apply, please send your CV at: hamid at irit dot fr
URL sujet détaillé : :

Remarques : The internship will be remunerated. It can be extended to a PhD grant on the same project.



SM207-32 Interplay of security and safety  
Admin  
Encadrant : Brahim HAMID
Labo/Organisme : IRIT
URL : https://www.irit.fr/~Brahim.Hamid/
Ville : Toulouse

Description  

In system engineering, security and safety may be compromised in several system layers and life cycle stages. Usually, security and safety are considered when design decisions are made, leading to potential conflict. This brings tremendous challenges during system design and integration. Just consider CPS and the added complexity and connectivity they offer. For example, the security of cars has already been compromised with the possibility to interact with different safety-related functionality, like releasing the brakes while driving. Thus, security and safety in CPS can only be addressed holistically.
The ideas of system architecture, safety and security modeling and analysis are not new [1], but to the best of our knowledge, the interplay and integration of system security, safety and the rest of the architecture has not been well addressed. In this work, we will focus particularly on the interplay between safety, security and the system architecture; we aim at providing methodological and tool support for their design in unison.
The patterns that are at the heart of our system and software engineering process reflect security and safety solutions at several levels of abstractions (e.g., different systems engineering life-cycle stages, different architecture layers). In our vision, a security or safety pattern [2,3] is a subsystem exposing pattern functionalities through interfaces and solutions behavior and targeting security and safety properties. In this project, we propose a preliminary modeling framework of security and safety properties of design patterns and some of their interplay primitives. The proposed interplay specification makes an attempt to model the resulting effect between security and safety attributes of two interacting patterns. The interplay specification structure can capture the results of combined security and safety specifications of two participating patterns in an interaction. The targeted security and safety modeling syntax will provide a simple formalism for specifying the security and safety properties of individual patterns on which the interplay relationship among patterns can be established. At the core of the framework is a set of Domain Specific Modeling Languages (DSML) and model transformations. Emphasis will be placed on formally defining abstract and concrete syntaxes, as well as the semantics of the modeling languages, e.g., by translation to existing formal languages. This will enable us to verify models using formal analysis.

Bibliography :

[1] Kriaa, S., Pietre-Cambacedes, L., Bouissou, M., Halgand, Y., 2015. A survey of approaches combining safety and security for industrial control systems. Reliability Engineering System Safety 139, 156=96178.

[2] Hamid, B., G=FCrgens, S., Fuchs, A., 2016. Security patterns modeling and formalization for pattern-based development of secure software systems. Innovations in Systems and Software Engineering, Springer 12 (2), 109=96140.

[3] Schmidt, H., J=FCrjens, J., 2011. Connecting Security Requirements Analysis and Secure Design Using Patterns and UMLsec. In: 23rd International Conference on Advanced Information Systems Engineering (CAiSE). Vol. 6741 of LNCS. Springer, pp. 367=96382.


To apply, please send your CV at: hamid at irit dot fr
URL sujet détaillé : :

Remarques : The internship will be remunerated. It can be extended to a PhD grant on the same project.



SM207-33 Alarm prediction via space-time pattern matching  
Admin  
Encadrant : Anne BOUILLARD
Labo/Organisme : Le stage sera co-encadré par Marc-Olivier Buob et Philippe Jacquet (Nokia-Bell-Labs) et Anne Bouillard (MdC, ENS).
URL : http://www.di.ens.fr/~bouillar/
Ville : Nozay or Paris (at LINCS)

Description  

Existing networks relies on more and more components and process more and
more messages. Finding root cause of a faulty behavior may be very complex
especially if several equipments are involved.

The challenge here is to find the alarm correlations without a priori
knowledge of the functioning of the processes seen as black boxes. For this
the plan is to use the statistic of the alarm generation in the network in
order to infer the correlations rules and finally to evaluate the probability
of the imminence of a major disruption. Furthermore the retro-causal analysis
of the correlations can also help of the identification of the root cause of
the major dysfunction and cure them before they occur.
URL sujet détaillé : http://www.di.ens.fr/~bouillar/Sujets/spacetimealarm-m2.pdf

Remarques : Le stage sera co-encadré par Marc-Olivier Buob et Philippe Jacquet (Nokia-Bell-Labs) et Anne Bouillard (MdC, ENS).

Possibilité de rémunération



SM207-34 Algorithmique pour les flots de liens  
Admin  
Encadrant : Clémence MAGNIEN
Labo/Organisme : LIP6 (CNRS, UPMC)
URL : http://www.complexnetworks.fr/
Ville : Paris

Description  

De nombreux réseaux nous entourent : réseaux sociaux, graphe du web, réseaux d'interactions
entre protéines, réseaux de co-occurrences de mots, échanges d'emails, etc. L'état de l'art a com-
mencé à proposer des solutions pour analyser la structure de ces réseaux afin de pouvoir répondre
à des questions comme : quels nóuds sont les plus importants ? le réseau peut-il être décomposé en
groupes cohérents ?
Dans le cas où les réseaux sont dynamiques, l'approche habituelle consiste à agréger l'information
sous forme de graphe. Pourtant, dans de nombreux contextes (trafic réseau, transactions financières,
communications entre individus, etc), on est confrontés à des données sous forme de flots de liens :
la donnée est essentiellement composée d'une série de triplets (A, B, t) indiquant que A a interagi
avec B à l'instant t (par exemple, la machine A a envoyé un paquet à la machine B, ou le compte
bancaire A a transféré de l'argent au compte B, la personne A a envoyé un message à la personne
B, etc).
L'algorithmique pour les flots de liens a ceci de fondamental qu'il n'est pas question dans ce cas
de calculer une propriété à chaque instant, mais bien de prendre en compte la nature intrinsèque-
ment en flot des données. Un exemple type est la connexité : à un instant donné très peu d'emails
sont échangés ; il n'y a donc pas de sens à calculer la connexité du réseau à cet instant ; par contre
il est possible à une information d'être transférée par une succession d'emails. On voit émerger une
notion d'accessibilité, et au-delà de connexité, dynamique.
Le but de ce stage est de participer à la définition de notions fondamentales pour la description
des flots de liens, et de proposer les algorithmes pour les calculer de manière efficace.
URL sujet détaillé : http://www.complexnetworks.fr/wp-content/uploads/2016/10/algo.pdf

Remarques :



SM207-35 clemence.magnien.fr  
Admin  
Encadrant : Robin LAMARCHE-PERRIN
Labo/Organisme : LIP6 (CNRS, UPMC)
URL : http://www.complexnetworks.fr/
Ville : Paris

Description  

The optimisation of large-scale sociotechnical services ( e.g. , transports, mobile com-
munication, web services) requires a deep understanding of users' interactions in several
domains (geographical mobility, social interactions, digital data exchanges) and at sev-
eral spacial and temporal scales (from individuals to nations, from seconds to years). In
this context, we aim at designing multiscale analysis methods to tackle the structural and
dynamical complexity of large interaction networks.
From a formal point of view, classical tools from graph theory allows to model static
networks, but they often fail to properly handle dynamical ones. This is because time
and space in complex systems are strongly inhomogeneous and should hence be carefully
handled. To that purpose, link streams constitute a new formalism to represent dynamical
networks as genuine spatio-temporal objects: Each interaction is represented as a triplet
(sender, receiver, time) allowing to fully describe the dynamics of interactions. From this
formalism, and with a multiscale perspective, we aim at identifying macroscopic interaction
patterns that properly summarise the microscopic link stream in order to reduce its de-
scriptional complexity. Such pattern could correspond to local but long-term interactions
( e.g. , in neighbourhood daily life), to global but short-term interactions ( e.g. , viral piece
of news on the internet), or to any combination of intermediate scales.
In previous work, we proposed several aggregation algorithms for multiscale analysis of
structured datasets, and in particular of hierarchical systems (for spatial aggregation) and
of interval sets (for temporal aggregation). These algorithms strongly rely on information-
theoretical measures to de=1Cne relevant scales for the analysis, by de=1Cning a trade-o=1B be-
tween descriptional complexity and information content of aggregated data. Intuitively,
the optimisation of this parametrized trade-o=1B results in (1) the aggregation of patterns
that are homogeneous in space and time and (2) the detection of irregularities that arise at
di=1Berent scales in the data. This research project aims at developing and applying similar
algorithms to the aggregation of link streams in order to provide consistent methods for
multiscale analysis of dynamic networks.
URL sujet détaillé : http://www.complexnetworks.fr/wp-content/uploads/2016/01/M2R_multilevel_networks.pdf

Remarques :



SM207-36 Analyse de Transactions Financières en Bitcoins  
Admin  
Encadrant : Matthieu LATAPY
Labo/Organisme : LIP6 (CNRS, UPMC)
URL : http://www.complexnetworks.fr/
Ville : Paris

Description  

Bitcoin est la première et la plus répandue des monnaies numériques décentralisées. Plus de 13
millions de bitcoins sont actuellement en circulation, ce qui correspond à plusieurs milliards d'Euros
(suivant les cours), et une centaine de milliers de commerçants l'acceptent dans le monde. Elle
repose sur une base de données pair-à-pair et publique issue d'une technologie appelée BlockChain.
Cette technologie a de nombreuses propriétés importantes, dont la transparence des transactions,
l'absence d'autorité centrale de régulation, un nombre maximal de bitcoins, etc.
Comme l'ensemble des transactions Bitcoin est disponible publiquement, cette plateforme offre
une opportunité unique pour l'étude de flux financiers. Elle contient plus de 100 millions
de transactions, et s'enrichit typiquement de plus de 100 000 transactions par jour (avec une forte
variabilité). Représenter cet ensemble de transactions par un graphe (comptes reliés par des tran-
sactions entre eux) est naturel et permet d'explorer diverses structures.
Ces représentations ne capturent toutefois pas la dynamique temporelle des transactions, qui
est essentielle pour comprendre l'activité sous-jacente. Nous proposons ici de représenter chaque
transaction par un flot de liens, c'est-à-dire une suite de triplets (t, u, v) indiquant qu'à l'instant
t une transaction a eu lieu entre u et v. Cette représentation a l'avantage de capturer à la fois la
structure des transactions (comme les graphes) et leur dynamique temporelle.
Afin de décrire ces flots de liens d'un point de vue à la fois structurel et temporel, il
s'agira en un premier temps de travailler à la généralisation aux flots de liens de plusieurs notions
classiques sur les graphes : degrés, densité, chemins, communautés, centralités, etc. Il s'agira ensuite
de calculer ces propriétés sur la masse des transactions bitcoins publiquement disponible, ce qui pose
des questions d'efficacité difficiles, et d'en tirer une description fine. On s'attachera en particulier
à identifier des événements dans cette dynamique, qu'on rapprochera d'événements connus
dans la sphère Bitcoin (comme par exemple des fraudes, des détournements, ou des événements
boursiers).
URL sujet détaillé : http://www.complexnetworks.fr/wp-content/uploads/2016/01/M2R_multilevel_networks.pdf

Remarques :



SM207-37 Conversations, Groupes et Communautés dans les Flots de Liens  
Admin  
Encadrant : Matthieu LATAPY
Labo/Organisme : LIP6 (CNRS, UPMC)
URL : http://www.complexnetworks.fr/
Ville : Paris

Description  

Un flot de liens est une suite de triplets (t, u, v) indiquant que les entités u et
v ont interagi à l'instant t. Il peut s'agir d'échanges de messages (emails par exemple)
entre individus, de transferts de paquets entre machines sur un réseau, d'achats en ligne
par des clients, d'appels téléphoniques, ou encore de contacts entre individus observés par
des capteurs. Les contextes pratiques où les données se modélisent naturellement comme
des flots de liens sont extrêmement nombreux. Ces objets sont donc cruciaux pour de nom-
breuses applications, notamment pour un large spectre de questions de sécurité (attaques
réseaux, connivences, fraudes, comportements malicieux, etc).
Dans tous ces contextes, des sous-flots jouent des rôles particuliers. Par exemple,
dans des échanges de messages, des sous-structures de discussions émergent naturellement
(comme des fils de discussion sur des listes de diffusion). Dans les contacts entre individus
observés par des capteurs, on retrouvera des réunions d'amis ou collègues. Dans des appels
téléphoniques ou des transferts de fichiers, on peut identifier une diffusion de rumeur ou
d'information. Enfin, dans du trafic réseau, les échanges entre machines participant à une
application distribuée (comme un système pair-à-pair ou un botnet par exemple) forment
de tels sous-flots. La figure ci-dessus illustre la modélisation de ces diverses réalités par des
flots de liens.
L'objectif central de ce projet est d'étudier les structures de sous-flots dans
les flots de liens.
URL sujet détaillé : http://www.complexnetworks.fr/wp-content/uploads/2016/01/M2R_multilevel_networks.pdf

Remarques :



SM207-38 Détection d'Attaques dans des Traces de Trafic Réseau  
Admin  
Encadrant : Matthieu LATAPY
Labo/Organisme : LIP6 (CNRS, UPMC)
URL : http://www.complexnetworks.fr/
Ville : Paris

Description  

Les attaques contre les services en ligne, les réseaux, les systèmes d'information, et les usur-
pations d'identité ont un coût annuel en milliers de milliards d'Euros et causent de nombreuses
faillites. Elles affaiblissent également la confiance des utilisateurs et ralentissent donc les progrès
de l'ère numérique.

Un des principaux moyens de lutte contre ces attaques consiste en l'observation du trafic
acheminé par le réseau et/ou reçu par les serveurs, en la détection du trafic induit par les attaques
et en l'analyse de ce trafic (pour le filtrer ou en trouver l'origine).

Les progrès en la matière sont aujourd'hui sévèrement limités par le manque de méthodes
et d'outils pour analyser les interactions au cours du temps. En effet, le trafic réseau peut
être vu comme une suite d'échanges entre machines au cours du temps, et une attaque est alors une
séquence d'interactions particulières dans cette suite. Voir figure ci-dessous pour une illustration.


Nous proposons ici de voir le trafic comme une suite de liens (t, u, v) indiquant le fait que les
machines u et v ont échangé un paquet à l'instant t. Nous souhaitons développer un ensemble de
notions permettant de décrire ces flots de liens de façon similaire à ce que la théorie des
graphes permet avec les réseaux : densité, degrés, chemins, centralité, ... Le premier défi est de
définir sur les flots de liens ces notions classiques en théorie des graphes.

Calculer ces propriétés sur des traces réelles posera des problèmes délicats d'efficacité : les
volumes de données sont énormes, typiquement des millions de liens par minute de trafic. Les
contraintes en temps et en mémoire nécessaires sont alors cruciales, et des approches originales
(comme du calcul en streaming) sont à explorer.
URL sujet détaillé : http://www.complexnetworks.fr/wp-content/uploads/2016/01/M2R_multilevel_networks.pdf

Remarques :



SM207-39 Évaluer la prévision de liens dans les graphes avec les distances de centralité  
Admin  
Encadrant : Lionel TABOURIER
Labo/Organisme : LIP6 (CNRS, UPMC)
URL : http://www.complexnetworks.fr/
Ville : Paris

Description  

Qu'il s'agisse de relations sociales, de transactions commerciales ou encore de machines
échangeant des paquets d'information, la structure des réseaux complexes auto-organisés évo-
lue au cours du temps. Les mécanismes microscopiques qui font que des liens se créent et
que d'autres disparaissent au cours du temps sont souvent mal identifiés. Par conséquent,
comprendre ce qui fait que telle interaction a plus de chance de se produire que telle autre
est un enjeu majeur pour comprendre la dynamique de tels systèmes.

Une manière simple et naturelle de résumer par une valeur numérique la qualité de la
prévision est de mesurer la distance d'édition du graphe (graph edit distance, ou GED) : oncompte le nombre de liens qui diffèrent entre le graphe attendu et le graphe observé. En pra-
tique, cela revient à faire la somme des faux positifs et des faux négatifs de la prévision. Cette
mesure semble judicieuse dans de nombreux contextes, cependant elle souffre de plusieurs
défauts. D'abord, elle ne fait pas de distinction entre les catégories de mauvaises prévisions.
Faux positifs et faux négatifs sont mis au même niveau alors que selon les applications, un
type d'erreur peut être beaucoup plus critique que l'autre. De plus, cette mesure ne fait pas de
différence entre les liens prévus alors que connecter deux nóuds très éloignés dans le graphe
a beaucoup plus d'impact sur son fonctionnement que connecter deux nóuds qui font déjà
partie de la même communauté.
URL sujet détaillé : http://www.complexnetworks.fr/wp-content/uploads/2016/01/M2R_multilevel_networks.pdf

Remarques : Co-encadrement entre le LIP6 (Paris) et le LAAS (Toulouse). Le stage peut-être effectué à l'un ou l'autre des laboratoires.



SM207-40 Génération aléatoire de graphes bipartis  
Admin  
Encadrant : Fabien TARISSAN
Labo/Organisme : ISP
URL : http://www.complexnetworks.fr/
Ville :

Description  

Dans de très nombreux contextes applicatifs, on rencontre de grands graphes
n'ayant aucune structure simple apparente, que nous appellerons graphes de terrain (par
opposition aux graphes explicitement construits par un modèle ou une théorie). Citons
par exemple la topologie de l'internet (routeurs et câbles entre eux), les graphes du web
(pages web et liens hypertextes entre elles), les échanges divers (pair-à-pair, e-mail, etc),
mais aussi les réseaux sociaux, biologiques ou linguistiques.
Il est apparu récemment que la plupart de ces grands graphes ont des propriétés statis-
tiques en commun, et que ces propriétés les différencient fortement des graphes aléatoires 1
utilisés jusqu'alors pour les modéliser. Notamment, ils ont une densité très faible, une dis-
tance moyenne faible, une distribution de degrés hétérogène, et une densité locale forte.
Depuis lors, de nombreux travaux ont été menés visant à capturer ces propriétés dans des
modèles, nécessaires tant pour effectuer des simulations que pour étudier formellement ces
objets, et bien sûr pour en comprendre la nature.
Les graphes aléatoires classiques capturent la densité faible (qui est en fait un paramètre
du modèle) et la distance moyenne faible. Par contre, ils ont une distribution des degrés
homogène et une densité locale faible. Nous sommes également en mesure de générer un
graphe aléatoire à distribution de degrés donnée. On capture ainsi toutes les propriétés
citées ci-dessus sauf la densité locale forte. Malgré de nombreuses tentatives, générer des
graphes ayant également une densité locale forte tout en gardant leur caractère aléatoire
reste un problème ouvert. Les attentes sont pourtant extrêmement fortes.

Bien que pertinente, la représentation des réseaux sous forme de
graphes ne permet pas de rendre compte de la complexité inhérente à la structure hiérar-
chique de la plupart des réseaux. Si on considère par exemple les réseaux d'acteurs qui
relient les acteurs d'un même film ou les réseaux de co-publications qui relient les auteurs
publiant ensemble, il est bien plus réaliste de relier les acteurs aux films dans lesquels ils
jouent, et les auteurs à leur articles. Cette remarque a amené la communauté scientifique
à s'intéresser aux graphes bipartis dans lesquels l'ensemble des nóuds est scindé en deux
ensembles disjoints, et> et ⊥ (par exemple les films et les acteurs), de façon à ce que les
liens relient des nóuds du premier ensemble à des nóuds du second. Cet objet fondamental
s'est révélé pertinent à la fois pour l'analyse et la génération aléatoire des graphes de
terrains.
URL sujet détaillé : http://www.complexnetworks.fr/wp-content/uploads/2016/10/generation.pdf

Remarques :



SM207-41 Opinion Dynamics and Political Conflicts in the Media  
Admin  
Encadrant : Robin LAMARCHE-PERRIN
Labo/Organisme : LIP6 (CNRS, UPMC)
URL : http://www.complexnetworks.fr/
Ville : Paris

Description  

Social media and the digitisation of news are having far-reaching effects
on the way individuals and communities communicate, organise, and express themselves.
Can the information circulating on these platforms be tapped to better understand and
analyse the enormous problems facing our contemporary society? Could this help us to
better monitor the growing number of social crises due to cultural differences and diverging
world-views? Studying the structure of debates in the public sphere requires sophisticated
methods for the analysis of information flows between individuals. How information is
shaped and broadcasted by mass media? How to describe the way opinions are discussed
in social media? Debates are often represented as complex entanglements of such social
interactions, embedded in space and time, and displaying a multilevel structure: From
individual to institutional discourses; From regional to international matters; From the
fast dynamics of media =93buzzes=94 to the slower dynamics of social controversies.

To address these challenging issues, this internships aims at devel-
oping new methods for the analysis of multidimensional and multilevel networks in social
sciences. Such methods could build on recent work in graph theory regarding the =93link
stream=94 representation of evolving networks, which provides a novel and intuitive formal-
ism for the spatio-temporal description of social interactions by focusing on their causal
structure (who interacts with whom, when) and concealing for a moment their content
(how, why, about what). Jointly, using information theory, these methods could integrate
recent developments in data aggregation to provide a macroscopic perspective on such in-
teraction structures: How can one achieve a global understanding of complex interaction
patterns? This internship does not require any preliminary knowledge about these two the-
oretical frameworks. However, it requires the capacity to work with abstract formalisms
in general, in order to build novel and consistent methods in computer science.
URL sujet détaillé : http://www.complexnetworks.fr/wp-content/uploads/2016/10/opinions.pdf

Remarques :



SM207-42 Bi-colored chain scheduling  
Admin  
Encadrant : Guillaume AUPY
Labo/Organisme : INRIA Bordeaux
URL : http://gaupy.org
Ville : Bordeaux

Description  

Applications running on hierarchical platform have to cope with different memory constraints. The goal of this internship would be to co-schedule different applications under I/O congestion.
In high performance computing (HPC), a significant percentage of the computing capacity of large-scale platforms is wasted because of interferences incurred by multiple applications that access a shared parallel file system concurrently (I/O). Furthermore, many HPC application have a periodic behavior. They consist of the repetition over time of two operations: some amount of computation followed by a volume of data transfered between the file system and the computing nodes.
In this work, we want to take a simple mathematical model called bi-colored chains to represents those applications.




The goal will be to propose strategies to manage those application at scale.
Eventually, the student will look at how to cope with the resource constraints of future HPC machines (such as energy efficiency, reliability, or network topology).

The student will work depending on their preference, either on the theoretical model of bi-colored chains with the goal of designing approximation algorithms, or focused on a more applied study with actual applications and implementations.
URL sujet détaillé : https://framadrop.org/r/3UNJGmGDek#+j3RVnlDOap7siBmL/YswgGowwQ2YEfuhJCfH//xjrQ
---------------------------------------------------------------------


Remarques :



SM207-43 Stages Technicolor Connected Home Rennes (STB, gateways, etc.) TCH_OFF_2017_001  
Admin  
Encadrant : Laurence PIQUET
Labo/Organisme : Technicolor France
URL : www.technicolor.com :
Ville : CESSON SEVIGNE

Description  


With more than 100 years of experience and innovation, Technicolor is a major actor in entertainment, software, and gaming worldwide. With strong historical ties to the largest Hollywood studios, the company is a leading provider of production, postproduction and distribution for creators and distributors of content. Technicolor is a world leader in film processing, a leading supplier in the field of decoders and gateways and one of the largest manufacturer and provider of DVD & Blu-ray discs. The recent acquisition of The Mill, a leading visual effects and content creation studio for the advertising, gaming and music industries adds one more first-rate brand to our already robust portfolio (MPC, Mikros Image and Mr. X), effectively making Technicolor the leader in VFX and post production services to the advertising production segment
The company also has a strong activity in Intellectual property and Licensing business.
This unique environment presents an exceptional opportunity to explore cutting-edge video technologies that will reach homes in the years to come. In Rennes research and development center, our engineers will make your internship a fascinating and rewarding experience.
For more information, please visit our website: www.technicolor.com
You can discover all our internship offers on:
http://www.technicolor.com/en/innovation/student-day/

Objectives /missions
Our interns' mission is to help R&D engineers enabling Multiple Play Video and Communications through:
- The design / supply of set-top box platforms to satellite, cable and telecom operators
- The design / supply of access devices to deliver multi-play services to subscribers

We offer internship opportunities in the multiple fields around:
o integrated solutions:
- Ultra HD - Multiscreen - OTT solutions

o Products & Software
- Video gateways - Set-top boxes - Modems & gateways - Software - Professional services

If you are interested in joining us, please visit our website to see the detailed internship open positions at : http://www.technicolor.com/en/innovation/student-day/internship-opportunities-connected-home/connected-home-internships


Profile
- Preferably Master 2 Student in engineering school / university
- Specialization in computing, software, system architecture, embedded real-time software development, testing, UI, etc.
- User =96Oriented mindset
- Inquiring mind, inventive, passionate.
- Good English level

To apply:

If you are interested in joining us, please visit our web site and consult our internship open positions at http://www.technicolor.com/en/innovation/student-day/internship-opportunities-connected-home/connected-home-internships

and apply at stage.rennes.com
Group: Technicolor (www.technicolor.com) / Connected Home Rennes.
Position: Intern -
Location: Rennes, FRANCE -
Deadline: Open.
Compensation: =801200 per month (before taxes)

Dépôt des offres / Contact

Consulter les offres sur http://www.technicolor.com/en/innovation/student-day/internship-opportunities-connected-home/connected-home-internships

Envoyer CV + LM à stage.rennes.com


URL sujet détaillé : http://www.technicolor.com/en/innovation/student-day/internship-opportunities-connected-home/connected-home-internships

Remarques : Compensation: =801200 per month (before taxes), Technicolor participe au transport en commun et au frais de déjeuner



SM207-44 Game Theory Algorithm for IT and Power reconciliation  
Admin  
Encadrant : Jean-marc PIERSON
Labo/Organisme : IRIT
URL : datazero.org :
Ville : Toulouse

Description  

This internship will be done in the context of the project Datazero, where renewable energies feed datacenters with power (see datazero.org).

In this project, an optimization is done from the IT infrastructure, basically trying to schedule jobs on computer servers to minimize both the makespan of the jobs and the energy consumed by the system.
Another optimization is done from the Power infrastructure in order to schedule the power production according to the renewable sources available, so as the lifetime and the quality of the power feeding is maximized.
To make these two worlds cooperate and find a tradeoff between these two optimization problems, the internship will investigate Game Theory and its usage in the context of this project. No a priori solution is favored at this stage, and innovative solutions can be envisioned by highly motivated and skilled candidates, either from a fundamental side or from a more applied side. Approaches providing exact or approximate solutions or groups of solutions can be investigated.


URL sujet détaillé : :

Remarques : A grant will be awarded during the internship.




SM207-45 A Cloning Approach to Social Network Anonymization  
Admin  
Encadrant : Frederic PROST
Labo/Organisme : LIG Université Grenoble Alpes
URL : https://perso.ens-lyon.fr/frederic.prost/
Ville : Grenoble

Description  

Internship Motivations

The information in social networks becomes an important data source, and sometimes it is necessary or beneficial to release such data to the public. Many real-world social networks contain sensitive information and serious privacy concerns on graph data have been raised. The famous result of Narayan and Shmatikov [3] has shown that naive anonymization does not work: it is in practise very easy to re-identify elements of a trivially anonymized (ie replacing identifying informations such as names, social security numbers etc. with random numbers) social networks. Later works [2] pushed further the study of attacks on anonymized social networks.

The goal of social network anonymization is to produce a graph in such a way that some statistical functions produce the same result on the original graph and on the transformed graph, while other functions (namely reidentification) should not produce the same result. There are two main ways to work on the anonymization:

Clustering: one tries to group together edges and nodes so that when the the cluster regroups then there is no way to distinguish an individual node among them.
k-anonymity: one tries to modify the original graph in such a way that there should be at least k-1 other candidate nodes with similar features (the features are part of the assumption made on the capability of the attacker).

Internship Objectives

The aim of the internship is to study a new approach to social data anonymization. The starting point is to use a graph rewriting approach based on category theory [1]. Using this approach it is very easy to make clones of a graph while being able to ``tune'' the properties of the clones. The idea is to select 1/k nodes, to make k-clones of this selection and to link them together in an appropriate way so that the global graph obtained shares good properties with relation to the original graph.

Location

This intership will be held at the LIG laboratory in Grenoble France in the team CAPP, coached by Frederic Prost.
Requisite skills and abilities

C++ programming
Graph theory.
Category Theory
Ability to use/modify large programs.

References

[1] Andrea Corradini, Dominique Duval, Rachid Echahed, Fr'ed'eric Prost, Leila Ribeiro: AGREE - Algebraic Graph Rewriting with Controlled Embedding. ICGT 2015: 35-51

[2] Lars Backstrom, Cynthia Dwork, Jon M. Kleinberg: Wherefore art thou R3579X?: anonymized social networks, hidden patterns, and structural steganography. Commun. ACM 54(12): 133-141 (2011)

[3] Arvind Narayanan, Vitaly Shmatikov: De-anonymizing Social Networks. IEEE Symposium on Security and Privacy 2009: 173-187
URL sujet détaillé : http://perso.ens-lyon.fr/frederic.prost/Internships/An_Ca.html

Remarques :



SM207-46 Automatically solving chess variants  
Admin  
Encadrant : Frederic PROST
Labo/Organisme : LIG Université Grenoble Alpes
URL : https://perso.ens-lyon.fr/frederic.prost/
Ville : Grenoble

Description  

Internship Motivations

The game of chess has often been presented as "unsolvable" due to the enormous size of the space search. Indeed, it is estimated that the number of legal positions of this game lies around 10^{43} and 10^{50}, and the number of interesting games is roughly 10^{120} (ref. Shannon number). These numbers have to be seen at the light of the number of atoms in the universe which is estimated to 10^{80}.

Nevertheless, using an hybrid human/computer approach, it has been possible to solve a smaller variant of chess on a 5x5 board (see [1]). The space search of this variant is around 10^{20}, roughly equivalent to that of the checkers game on 8x8 board (see [2]). A small web site has been made to gather informations on the solved variants of chess: Mini Chess Resolution.

We have developped some ideas to completely automatize the proof search.

The aim of the internship is to work them on and implement these ideas and ulitmately to test them on several variants of chess (notably Los Alamos chess and atomic chess).

Internship Objectives

The aim of the internship is to implement an oracle finder in a distributed way. More precisely:

Implement an oracle finder that starting from a position builds a formal proof of the theoretical value of the position.
Implement a mate finder based on asymetrical search once an unbalanced position is reached.
Conduct tests to find heuristics in order to downsize the size of the oralces produced. Further researches could investigate machine learning in order to find out those heuristics autmatically.

Location

This intership will be held at the LIG laboratory in Grenoble France in the team CAPP, coached by Frederic Prost.

Requisite skills and abilities

C++ programming
Artificial Intelligence
Ability to modify large programs (typically stockfish)
Curiosity...

References

[1] M. Mahlla and F. Prost. Gardner's minichess is solved. International Computer Games Association Journal, 2013. International Computer Games Association Journal, 36(4), 2013. Article available here.

[2] Jonathan Schaeffer, Neil Burch, Yngvi Bj"ornsson Akihiro Kishimoto, Martin M"uller, Robert Lake, Paul Lu and Steve Sutphen. Checkers Is Solved. Science Vol. 317, Issue 5844, pp. 1518-1522, 2007. Article available here.
URL sujet détaillé : http://perso.ens-lyon.fr/frederic.prost/Internships/Chess.html

Remarques :



SM207-47 Matching algorithms for dynamically changing bipartite graphs  
Admin  
Encadrant : Bora UÇAR
Labo/Organisme : ROMA, LIP, Ens Lyon
URL : http://perso.ens-lyon.fr/bora.ucar/
Ville : Lyon

Description  

A matching in a graph is a subset of edges no two sharing a common vertex. A perfect matching is a matching where all vertices are on a matching edge. Given a bipartite graph with edge weights, the bottleneck value of a matching is defined as the minimum weight of an edge in that matching. The maximum bottleneck perfect matching (MBPM) problem asks for a perfect matching having the maximum bottleneck value. The MBPM problem is efficiently solvable in polynomial time for a given bipartite graph.

This internship is concerned with dynamically changing bipartite graphs. Suppose we have an edge weighted bipartite graph and a maximum bottleneck perfect matching, and suppose that the edge weights undergo slight changes. How fast can we compute a new maximum bottleneck perfect matching under the new edge weights? What about the next one, and the next say k of them, where k is a much smaller than the number of vertices. The internship will seek answers to these questions. The intern will help in designing, analyzing, and potentially implementing algorithms.

The internship requires theoretical and algorithmic background; in particular graph theory and algorithms, amortized analysis of algorithms, and probabilistic reasoning will likely be very useful.

URL sujet détaillé : :

Remarques : This is a paid internship, as regulated by the law.



SM207-48 Amélioration d'un outil d'ingénierie dirigée par les modèles pour la réalisation d'applications de supervision de réseaux de capteurs et d'actionneurs  
Admin  
Encadrant : Jérôme ROCHETEAU
Labo/Organisme : ICAM
URL : http://www.icam.fr/research/our-researchers
Ville : Carquefou

Description  

L'ICAM est une école d'ingénieurs Arts et Métiers située à Carquefou. Ses enseignants chercheurs participent à des projets de recherche appliquée en collaboration avec des partenaires industriels et universitaires. Dans le cadre de ses activités de recherche, le site de l'ICAM héberge deux démonstrateurs de systèmes dits intelligents. Il s'agit, d'une part, d'une expérimentation interne concernant la supervision de la température, de l'humidité et du chauffage déjà installée dans les bâtiments. Il s'agit, d'autre part, d'un démonstrateur d'éclairage intelligent en cours d'installation dans le cadre d'un projet de recherche européen. L'ICAM a ainsi développé un prototype qui génère des services web pour la supervision (SCADA) d'un réseau de capteurs et d'actionneur (SAN) à partir d'un modèle de ce réseau.

Bien que ce prototype apporte la preuve de la pertinence d'une approche dirigée par les modèles dans le contexte des systèmes dits intelligents, il se cantonne à ce jour aux fonctionnalités essentielles d'une application SCADA (communication avec les capteurs et actionneurs, acquisition de données, contrôle automatique) et est limité à cause de l'absence :

=97 d'une prise en compte des utilisateurs, de leurs rôles et de leurs droits d'accès,

=97 d'une interface web générique pouvant s'appliquer aux différentes applications générées,

=97 d'une étude comparative avec des applications SCADA comme PCVue.

La mission de ce stage consiste ainsi à pallier ces différentes absences conjointement. Le prototype pourra être éprouvé en continu sur les deux démonstrateurs disponibles sur le site même de l'ICAM. La mission consiste idéalement à valoriser les résultats de ce stage à travers une publication scientifique dans une conférence internationale.
URL sujet détaillé : :

Remarques : Nature du stage : recherche et développement (R&D)

Mots-clés : model-driven development (MDD), supervisory control and data acquisistion
(SCADA), sensor and actuator network (SAN), model-to-model transformation (M2M)

Gratification : entre 537,60=80/mois et 900=80/mois



SM207-49 February-August 2017 (flexible)  
Admin  
Encadrant : Alexandra SILVA
Labo/Organisme : Univeristy College London
URL : http://pplv.cs.ucl.ac.uk/welcome/
Ville : London, UK

Description  

Automata are a well established computational abstraction with a wide range of applications, including modelling and verification of (security) protocols and state-based systems. In an ideal world, a model would be available *before* a system/protocol is deployed: in this way, relevant properties may be checked first, and only then the actual system would be synthesized from the verified model. Unfortunately, this is not at all what happens in reality. Systems/protocols are developed and coded in short spans of time: if mistakes occur they are most likely found after deployment. In this context, it has become popular to infer, =91'learn'' a model from a given system just by observing its behaviour or response to certain queries. The learned model can then be used to ensure the system is complying to desired properties, or detect bugs and design possible fixes.

Automata learning is a widely used technique for creating an automaton model from observations. The original algorithm, by Dana Angluin, works for deterministic finite automata, but since then has been extended to other types of automata, including Mealy machines and I/O automata, and even a special class of context-free grammars. Motivated by practical applications such as XML processing and program trace analysis, where values for individual symbols are typically drawn from an infinite domain, a new algorithm was recently proposed (and implemented) for automata over infinite alphabets.

The goal of this project is to take the algorithm and its implementation to a new level of applicability. In particular, we want to look at possible improvements in the data structures used in the implementation to speed up the learning process. More interestingly, we want to apply the new algorithm to real case studies. One possibility is to learn (and possibly find bugs) in the implementation of protocols such as TCP/IP.

This project is supervised jointly with Fabio Zanasi and Matteo Sammartino. Feel free to email us for more details.
URL sujet détaillé : :

Remarques :



SM207-50 In Situ Data Analysis for Large Parallel Simulations  
Admin  
Encadrant : Bruno RAFFIN
Labo/Organisme : INRIA
URL : https://team.inria.fr/datamove/
Ville :

Description  

Location: University Grenoble Alpes Campus, Saint Martin D'heres (close to Grenoble)
Duration: At least 4 months, possibility to pursue as a PhD.
Contact: Bruno.Raffin.fr and frederic.wagner.fr
Incomes: Gratifications de stage (about 500 euros/month)

Next generation supercomputers will enable to run very large scale simulations producing huge data sets. Handling these data from their locus of production in the nodes of the supercomputer, up to the analysis and their visualization is a key challenge. Instead of processing the data for compression, indexing, analysis and visualisation once saved on disks (Post-Processing), the so called In Situ processing paradigm proposes to start data processing directly in the nodes where the application runs, while the data are still in memory. This research domain, at the intersection between Big Data processing and Exascale computing, is recognized as crucial for very large scale simulations on next generation supercomputers[5].

At INRIA, our team, Datamove is investigating new approaches for In Situ analytics. We developed FlowVR, a very flexible environment to experiment witha large variety of In Situ scenarios. We also developed several in situ analytics scenarios based on molecular dynamics or fluid simulations [2,3].

Today's approach inherit from the traditional schema where the application decides when to push results to the file system. The goal of this intership is to explore a new approach where the simulation is actually under the control of the analytics framework: the analysis decides when and what data to extract from the running simulation according to the analysis to be performed. Analysis can be as simple as writing the raw data extracted from the simulation to a permanent storage or processing these data (compression, indexation, computation of high level descriptors) before to save or directly visualize them.

We propose to start from the following baseline for exploring the potential of this approach:
- Data extraction:
We intend to extract data transparently from running applications with the use of debugging techniques.
Using both hardware and software breakpoints around data-modifying routines we should be able to extract
transparently and on the fly data from running processes. It should even be possible to reduce data in place (from
example computing statistics like variance) without any additional copy of the original data. Additionaly we hope to cover data-acquisition with computations, thus inducing virtually zero waiting times for the original application.
- Injection in distributed shared memory:
Extracted data will then be re-routed to a distributed shared memory layer using existing libraries. Both reader processes and visualization processes should be able to be stopped and started at any time without shutting down the memory layer.
- Performance analysis:
One key part of this work is based on performance analysis. Different options are available for the implementation
of data acquisition tools. For example it is clear that software breakpoints inccur a higher cost than hardware breakpoints. An in depth performance analysis is required in this work for all proposed solutions.



The intership will take place at the Datamove team located in the IMAG building on Saint Martin D'Heres University. She/he will be co-advised by Bruno Raffin and Frederic Wagner. The candidate will have access for her/his experiments to large computers (Grid'5000 and CIMENT). Beyond this intership, the candidate can pursue a PhD on this topic (funding not guaranteed yet)

For further information contact Bruno.Raffin.fr and Frederic.Wagner.fr

References:

[1]Theophile Terraz, Bruno Raffin, Alejandro Ribes and Yvan Fournier; "In Situ Statistical Analysis for Parametric Studies", Second Workshop on In Situ Infrastructures for Enabling Extreme-Scale Analysis and Visualization, SC'16, 2016, Salt Lake City.
[2] Matthieu Dreher, Bruno Raffin; =93A Flexible Framework for Asynchronous In Situ and In Transit Analytics for Scientific Simulations=94, 14th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing (2014). (http://hal.inria.fr/hal-00941413/en)
[3] Matthieu Dreher, Jessica Prevoteau-Jonquet, Mikael Trellet, Marc Piuzzi, Marc Baaden, Bruno Raffin, Nicolas Férey, Sophie Robert, Sébastien Limet. " ExaViz: a Flexible Framework to Analyse, Steer and Interact with Molecular Dynamics Simulations=94, Faraday Discussions of the Chemical Society (2014) (http://hal.inria.fr/hal-00942627/en)
[4] C. Docan, M. Parashar, and S. Klasky, =93DataSpaces: an Interaction and Coordination Framework for Coupled Simulation Workflows,=94 Cluster Computing, vol. 15, no. 2, pp. 163=96181, 2012.
[5] Synergistic Challenges in Data-Intensive Science and Exascale Computing. US Department of Energy, March 2013 (http://science.energy.gov/~/media/40749FD92B58438594256267425C4AD1.ashx).
[6] F. Zheng, H. Zou, G. Eisnhauer, K. Schwan, M. Wolf, J. Dayal, T. A. Nguyen, J. Cao, H. Abbasi, S. Klasky, N. Podhorszki, and H. Yu, =93FlexIO: I/O middleware for Location-Flexible Scientific Data Analytics,=94 in IPDPS'13, 2013.
[7] M. Dorier, G. Antoniu, F. Cappello, M. Snir, and L. Orf. =93Damaris: How to Efficiently Leverage Multicore Parallelism to Achieve Scalable, Jitter-free I/O,=94 in CLUSTER =96 IEEE. International Conference on Cluster Computing. IEEE, Sep. 2012.
[8] M. Dorier, S. Ibrahim, G. Antoniu, R. Ross. Omnisc'IO: A Grammar-Based Approach to Spatial and Temporal I/O Patterns Prediction. Accepted, to appear in Proc. of ACM/IEEE SC 2014 (New Orleans, November 2014.
[9] Fang Zheng, Hongfeng Yu, Can Hantas, Matthew Wolf, Greg Eisenhauer, Karsten Schwan, Hasan Abbasi, Scott Klasky. GoldRush: Resource Efficient In Situ Scientific Data Analytics Using Fine-Grained Interference Aware Execution. Proceedings of ACM/IEEE Supercomputing Conference (SC'13), November, 2013.

URL sujet détaillé : :

Remarques : Co-advised with Frederic Wagner (frederic.wagner.fr)



SM207-51 Extensions of certificate generation for roundoff error analysis  
Admin  
Encadrant : Eva DARULOVA
Labo/Organisme : Max Planck Institute for Software Systems (MPI-SWS)
URL : http://www.mpi-sws.org/~eva/
Ville : Saarbruecken

Description  

Being able to soundly estimate roundoff errors in floating-point computations is important for many applications in embedded systems and scientific computing.
Due to the unintuitive nature of floating-point arithmetic, automated static analysis tools show the most practical promise for this task. Their results, however, are only as correct as their implementation.
We are working on a new modular framework for the analysis of finite-precision computations which computes sound roundoff error bounds fully automatically and at the same time, generates a correctness certificate which can be checked independently, thus providing more confidence in the analysis results.
Currently, the certificate generation works only for a simple special case and the goal of the project is to extend it to more complex and also more useful cases, e.g. more advanced static analyses and mixed-precision.
The project involves work on the framework itself as well as work within a theorem prover (Coq or HOL Light).
URL sujet détaillé : :

Remarques : This project is taken by Raphaël Monat.



SM207-52 sparse polynomials and combinatorial geometry  
Admin  
Encadrant : Pascal KOIRAN
Labo/Organisme : LIP
URL : http://perso.ens-lyon.fr/pascal.koiran/
Ville : Lyon

Description  

In algebraic complexity the tau conjecture for Newton polygons is a conjecture about the number of vertices of Newton polygons of bivariate polynomials presented in a certain " succint " form, namely, as sums of products of sparse polynomials. It implies a separation of the complexity classes VP and VNP (this is arguably the main open problem in algebraic complexity theory). One goal of the internship will be to study special cases of the tau conjecture. For instance, if the polynomials f and g have t monomials each, how many vertices can we have on the Newton polygon of f.g+1?

One could also study some versions of the conjecture with an even more combinatorial flavour, for instance, the " onion peeling " of Minkowski sums. For two sets of t points E and F in the plane, their Minkowski sum E+F has at most 2t points on its convex hull. These points form the first layer of the onion. But how many point can we have, say, on the 10th layer ? The study of such questions could be guided by computer experimentations.

We also offer to work during this internship on another unrelated topic about sparse (univariate) polynomials: algorithms for deciding the existence of real roots, and possibly approximating these roots. Recent progress was made in particular in papers by Michael Sagraloff, but some basic questions remain unsolved. For instance, can we decide the existence of real roots for a polynomial f with, say, 4 monomials, in time polynomial in the sparse representation of f?

URL sujet détaillé : :

Remarques :



SM207-53 Transparence des algorithmes  
Admin  
Encadrant : Daniel LE MÉTAYER
Labo/Organisme : INRIA
URL : http://planete.inrialpes.fr/people/lemetayer/
Ville : LYON

Description  

Avec le développement massif de la collecte et de l'analyse de données, chacun se retrouve soumis de façon croissante à des algorithmes informatiques, généralement sans maîtriser ou même comprendre la logique de leurs traitements. De tels algorithmes interviennent notamment dans les moteurs de recherche, les systèmes de recommandation, les activités commerciales, l'enseignement, la santé, l'information, etc. Parce qu'ils ont des effets sur les personnes, ces traitements algorithmiques posent de façon renouvelée des questions sur la liberté de choix des individus, et peuvent induire des questions ou des doutes en matière de discrimination ou de loyauté.
Un des enjeux majeurs en la matière est celui de la " transparence " des algorithmes ou plus précisément la possibilité d'expliquer, voire de justifier leurs résultats. Il s'agit d'un domaine nouveau du point de vue de la recherche, même s'il peut s'appuyer sur des travaux bien établis, notamment dans le domaine du logiciel. Les leviers d'action possibles peuvent se classer en plusieurs catégories selon que l'on puisse agir sur le code des algorithmes (" transparency by design "), y avoir simplement accès (analyse en " boîte blanche ") ou pouvoir en observer seulement les résultats (analyse en " boîte noire "). L'objectif du stage est double :
1. Analyser les travaux dans le domaine de la transparence, notamment les plus récents (explicabilité des algorithmes, audits, etc.)
2. Analyser l'applicabilité des résultats existants aux différents types d'algorithmes (notamment d'apprentissage)
3. Evaluer la faisabilité de méthodes génériques reposant sur des notions de causalité pour estimer l'impact des données d'entrée sur les résultats.

URL sujet détaillé : :

Remarques : Références :

Anupam Datta, Shayak Sen, Yair Zick, "Algorithmic Transparency via Quantitative Input Influence: Theory and Experiments with Learning Systems", 2016 IEEE Symposium on Security and Privacy (SP), vol. 00, no. , pp. 598-617, 2016, doi:10.1109/SP.2016.42, https://www.andrew.cmu.edu/user/danupam/datta-sen-zick-oakland16.pdf

Kareem El Gebaly, Parag Agrawal, Lukasz Golab, Flip Korn, Divesh Srivastava:
Interpretable and Informative Explanations of Outcomes. PVLDB 8(1): 61-72 (2014)
http://www.vldb.org/pvldb/vol8/p61-elgebaly.pdf


Alex A. Freitas. 2014. Comprehensible classification models: a position paper. SIGKDD Explor. Newsl. 15, 1 (March 2014), 1-10.
http://delivery.acm.org/10.1145/2600000/2594475/p1-freitas.pdf?ip=134.214.254.200&id=2594475&acc=ACTIVE%20SERVICE&key=7EBF6E77E86B478F%2E399DC7EE7AC85DEE%2E4D4702B0C3E38B35%2E4D4702B0C3E38B35&CFID...6895534&CFTOKEN=87766734&__acm__=1477402633_9d86bfb5b2b79ce8bc164d7804093bf1

EPIC : https://epic.org/algorithmic-transparency/




SM207-54 HOW TO EVALUATE THE COMPLIANCE OF A SECURITY EVENT FLOW SETUP TO SLAS  
Admin  
Encadrant : Christine MORIN
Labo/Organisme : IRISA/Inria
URL : https://team.inria.fr/myriads/
Ville : Rennes

Description  

Infrastructure as a Service (IaaS) clouds use virtualisation to allow tenants to outsource their information systems in the provider's cloud. Key characteristics of IaaS clouds include scalability, multi-tenancy and resource sharing.
One of the risks of moving to a public cloud is losing full control of the information system infrastructure. The provider will be in charge of monitoring the physical infrastructure and providing the required service to clients. This pushes clients to have trust on providers. Providers give assurance on some aspects of the
service but, as of today, security monitoring is not one of them. In our work, we aim to allow providers to provide customers with guarantees on security monitoring of their outsourced information system.
We focus our work on security monitoring in clouds. Security Monitoring is the collection, analysis, and escalation of indications and warnings to detect and respond to intrusions. By monitoring a system it is possible to detect suspicious behaviors and take action before severe damage.
A security monitoring framework is based on probes in the information system, like Intrusion Detection Systems (IDS). Probes generate security logs that are processed by several tiers until they reach the security operator. The intermediate
tiers are composed of log collectors and aggregators, which configurations, numbers, and locations in the network must be carefully chosen to achieve required properties like timeliness and reliability.
In an IaaS cloud, the security monitoring frameworks of the tenants are partly implemented by the provider outside of the virtualized information systems, so that components like IDSes and log collectors may be less vulnerable to attacks and can be shared between tenants. Thus the provider has to automatically configure
security monitoring components for the tenants.
A Service Level Agreement (SLA) is a contract between clients and service providers. SLAs describe the provided service, the rights and obligations of both parties and state penalties for when the specified terms are not respected. Hence, SLAs help providers to build more trust.
To include security monitoring terms into an IaaS cloud SLA, the following tasks are required:
(1) a way for providers/clients to specify their security monitoring parameters/requirements,
(2) mechanisms to enforce these requirements in a cloud infrastructure,
(3) a verification method to check if the requirements are respected at any
given time.
The purpose of this internship is to study IaaS cloud SLA security monitoring terms related to the intermediate tiers of security log management. This should extend the work in progress about security monitoring terms related to a network IDS. The student's objectives are:
(1) to find relevant metrics to describe the compliance to SLAs of a setup of the log collection and aggregation tiers in the provider part of the security monitoring frameworks;
(2) to design methods for a tenant to verify online that the provider has setup the collection and aggregation tiers correctly according to the SLA terms;
(3) to implement and evaluate a selection of the verification methods designed.
URL sujet détaillé : https://team.inria.fr/myriads/files/2016/09/topic.pdf

Remarques : Internship co-advised with Louis Rilling and Amir Teshome.



SM207-55 Discrétisations de plan et symétrie rotationnelle  
Admin  
Encadrant : Thomas FERNIQUE
Labo/Organisme : LIPN
URL : https://lipn.univ-paris13.fr/~fernique/
Ville : Villetaneuse

Description  

One of the main method to define quasiperiodic tilings is the cut and project scheme. It consists in digitizing a subspace of a higher dimensional space.
For example, Sturmian words can be obtained by digitizing an irrational line of the Euclidean plane, and Penrose tilings by digitizing an algebraic plane in the five dimensional space.

Another prominent method to define quasiperiodic tilings is the substitution process. It consists in inflating each tile which is then decomposed in a set of original tiles. Penrose tilings can be obtained by substitution, but not every Sturmian words (only those defined by a line with a quadratic slope).

The general goal of this internship is to better understand the connection between these two methods. In particular, Kari and Rissannen have recently found a substitution process to obtain tilings with a rotational symmetry of any even order: can we also obtain these tilings by a cut and project scheme?

Short bibliography:

1) The paper of Kari and Rissannen:
https://arxiv.org/abs/1512.01402

2) A Ph.D thesis which characterize a particular class of cut and project tilings (the canonical ones) which can be obtained by a substitution process:
http://www.mathematicians.org.uk/eoh/files/Harriss_Thesis.pdf

3) A generic way to define substitutions:
http://iml.univ-mrs.fr/~arnoux/NonPisotAut.pdf
URL sujet détaillé : :

Remarques :



SM207-56 Learning for Signal Flow Graphs  
Admin  
Encadrant : Fabio ZANASI
Labo/Organisme : University College London - Programming Principles, Logic and Verification group (PPLV)
URL : http://pplv.cs.ucl.ac.uk/welcome/
Ville : London

Description  

Signal flow graphs are a well established family of signal processing circuits that play a foundational role in Control Theory. One intriguing aspect of the mathematics underpinning these structures is that they can be explained in terms of equivalent, yet seemingly diverse computational models, including rational stream functions and weighted automata.
This project aims at exploiting the correspondence with weighted automata to study signal flow graphs with automata-theoretic methods. The focus will be on learning, a technique that allows to synthesise an automaton recognising a certain language just by observing its behaviour or response to certain queries. Does the learning algorithm translate to a signal flow graph synthesis procedure in an interesting way? As signal flow graphs translate to particularly simple weighted automata (on a singleton alphabet), does the learning algorithm simplify too? Does it have a better complexity bound than for arbitrary weighted automata?

We will try to investigate these questions based on recent works that formulate both the theory of signal flow graphs and of automata learning in the abstract language of categorical algebra and coalgebra:

=97 Rutten - A Tutorial on Coinductive Stream Calculus and Signal Flow Graphs - Theoretical Computer Science, 2005.
=97 Bonchi, Sobocinski, Zanasi - The Calculus of Signal Flow Diagrams I: Linear Relations on Streams - Information and Computation, 2016.
=97 Jacobs and Silva - Automata Learning: a Categorical Perspective - P. Panangaden's Festschrift, 2014.

This project is jointly supervised with Alexandra Silva.
URL sujet détaillé : :

Remarques : This project is jointly supervised with Alexandra Silva.



SM207-57 Wagner  
Admin  
Encadrant : Pierre JOUVELOT
Labo/Organisme : MINES ParisTech
URL : https://www.cri.ensmp.fr/offres_stages.html#annonce2016-6
Ville : Paris

Description  

The ANR FEEVER project intends to foster the development of the
Faust functional programming language and ecosystem for efficient
digital audio signal processing.

In order to study certain formal properties and extensions of Faust
programs --- such as operational behavior or program logics --- we
have introduced the Wagnerww language, a functional synchronous language.

Wagner thus acts as a high-level intermediate target language for
the Faust compiler --- available in an experimental branch ---
but can be also related to a formal version of more recent
developments such as the MathWorks Audio System Toolbox. We
propose the three following lines of work:

- Typing and Semantics: Wagner type system is based on
co-effects and a simple notion of type polarity, with a
straightforward operational semantics, and an efficient virtual
machine related to the original semantics via logical relations.

You will work with us in extending the type system and improving the
operational semantics and proofs. Students should be familiar with
the theory of type systems for functional programming languages.

- Mechanized Semantics:

We have developed a basic Wagner model mechanized in Coq-MathComp,
enough to already prove quite interesting properties.
You will extend this model to accommodate some additional features,
as well as complete the part pertaining to Wagner's VM.

Some proficiency in Coq plus a basic understanding of the
Mathematical Components library is recommended. We'd be happy
however to take a candidate willing to learn the library.

- Type Inference and Compilation: We have developed a preliminary
OCaml-based compiler for Wagner; the compiler is capable of
performing some basic type inference and code generation. You will
work on improving the type inference strategy by adding
bidirectional type checking, and fine tuning the current interpreter for
Wagner's VM.

Familiarity with Ocaml and type inference is recommended.

URL sujet détaillé : https://www.cri.ensmp.fr/people/gallego/docs/wagner-2016.pdf

Remarques : The stage is co-advised with Emilio J. Gallego Arias.

The stage is renumerated, check the laboratory page for more details.



SM207-58 jsCoq  
Admin  
Encadrant : Pierre JOUVELOT
Labo/Organisme : MINES ParisTech
URL : https://www.cri.ensmp.fr/offres_stages.html#annonce2016-7
Ville : Paris

Description  

The jsCoq project is a port of the Coq proof assistant to the web
browser platform. jsCoq allows to write web pages with embedded
proof scripts, opening up significant new possibilities of
interaction and distribution. We propose two main lines of work:

- Coq Backend: the SerAPI protocol is an new protocol for
machine-based interaction with Coq, used in jsCoq, PeaCoq, and
experimentally by CoqIDE. We propose to extend the protocol in
two ways: a) improve the control protocol to better suit
document-oriented environments such as Emacs or the Web DOM; b)
improve the query subprotocol, which powers code completion,
display, and proof analysis tools.

- Web Frontend: we propose to integrate the frontend with
IPython's web libraries, to improve integration with
documentation generation tools, and to improve search, pattern,
type, and goal display.

We are open to other ideas. All our projects are open source and
available at github.

Desirable Requisites:
====================
Basic familiarity with Coq and proof workflow. Particular requisites
for each part are:

- Coq Backend: Fluency in Ocaml is recommended.
- Web Frontend: Fluency in JavaScript and UI web libraries is recommended.

URL sujet détaillé : https://www.cri.ensmp.fr/people/gallego/docs/jscoq-2016.pdf

Remarques : The stage is co-advised with Emilio J. Gallego Arias.

The stage is renumerated, check the laboratory page for more details.



SM207-59 Sorting genomes with colored block extremities  
Admin  
Encadrant : Krister SWENSON
Labo/Organisme : LIRMM
URL : http://www.lirmm.fr/~swenson/
Ville : Montpellier

Description  

Twenty five years of work by the computer science community has resulted in a host of models and algorithms for finding "sorting" scenarios of gene orders of genomes. However, parsimony has been the sole criterion for judging the relevance of these scenarios; one scenario is better than another if it has fewer sorting moves. The state-of-the-art works on colored genomes where the colors represent regions between genomes that are more likely to participate in the same move. The new questions ask which scenarios use the minimum number of moves acting on regions of different color, or out of all parsimonious scenarios, one that has the minimum number of moves acting on regions of the different color.

This project asks similar questions about genomes where colors are assigned to extremities of genes, rather than the regions between the extremities. We will study the relationship between the new and the old model, exploring new algorithmic insights when necessary.
URL sujet détaillé : :

Remarques :



SM207-60 Le problème du Domino à origine fixée sur un groupe  
Admin  
Encadrant : Nathalie AUBRUN
Labo/Organisme : LIP
URL : http://perso.ens-lyon.fr/nathalie.aubrun/
Ville : Lyon

Description  

Les tuiles de Wang sont des carrés unitaires portant une couleur sur chaque arête. Si une tuile de Wang, on appelle t_N (resp. t_S, t_E, t_W) la couleur portée par l'arête nord (resp. sud, est, ouest) du carré. On peut assembler des tuiles de Wang si elles portent la même couleur sur leur côté commun, et produire ainsi des pavages finis ou infinis du plan. Partant d'un jeu de tuiles fini t, on notera X_t l'ensemble des pavages valides du plan par t. On remarquera que cet ensemble peut être vide. Un résultat célèbre dû à Berger (1966 (dont la preuve sera ensuite simplifiée par Robinson (1971)) montre qu'on ne peut pas décider le problème de la pavabilité par un jeu de tuile de Wang (aussi appelé problème du Domino, noté DP dans la suite).


En assimilant le plan quadrillé au groupe Z^2, un pavage du plan par t devient une application x:Z^2 -> t qui vérifie les règles de voisinage. Remplaçons à présent Z^2 par un groupe G engendré par les générateurs s_1,...,s_k et les carrés de Wang par des polygones à 2k côtés : on peut ainsi définir des pavages sur le groupe G par un jeu de tuiles t fini. Les mêmes questions que sur Z^2 se posent, notamment celle de caractériser les groupes sur lesquels DP est décidable. Cette question, difficile, a conduit à la formulation de la conjecture suivante : DP est décidable sur le groupe et seulement si G est virtuellement libre (Ballier & Stein, 2013).


Une variante, plus faible, du problème du Domino est le problème du Domino à origine fixée OCDP. Cette fois-ci, on s'interroge sur l'existence d'un pavage valide en imposant à une tuile donnée d'apparaître à l'origine. Clairement, si ce problème est décidable, alors il en est de même pour DP (il suffit de lancer en parallèle l'algorithme résolvant OCDP pour chacune des tuiles du jeu de tuiles). Cependant, on ne sait rien sur l'implication réciproque.


L'objectif du stage est de se concentrer sur le problème à origine fixée. Il s'agira dans un premier temps de démontrer son caractère indécidable sur des exemples de groupes bien choisis (groupes de surface, ou groupe de l'allumeur de réverbères par exemple). Les preuves connues sur Z^2, que l'on peut adapter à certains groupes ou structures (Robinson 1978, Kari 1999, Aubrun & Kari 2013), sont basées sur un encodage de système calculant simple (machine de Turing ou bien fonctions affines par morceaux). Une autre motivation du stage est de chercher, parmi les résultats d'indécidabilité connus (problème de l'arrêt pour les machines de Minsky à 2 compteurs, problème de correspondance de Post, etcdots), ceux pour lesquels on peut trouver une réduction vers OCDP.

Prérequis :

Des connaissances de base en théorie des groupes ainsi qu'une bonne familiarité avec la théorie de la calculabilité sont fortement souhaitées.

Objectifs du stage :
- Montrer que OCDP est indécidable sur les groupes de surface, le groupe de l'allumeur de réverbères.
- Trouver de nouvelles réductions pour montrer l'indécidabilité de OCDP.
- Pour quels groupes a-t-on l'équivalence "DP décidable <=> OCDP décidable" ?


URL sujet détaillé : http://perso.ens-lyon.fr/nathalie.aubrun/stage_M2_2017.pdf

Remarques : Possibilité de poursuite en thèse.



SM207-61 Energy efficient scheduling for highly heterogeneous cloud infrastructure  
Admin  
Encadrant : Patricia STOLF
Labo/Organisme : IRIT
URL : http://www.irit.fr
Ville : Toulouse

Description  

The energy consumption of cloud infrastructures represents a more and more important part in the world energy consumption. Most of the time, these infrastructures are oversized with regard to needs and servers are rarely used in their maximal capacity. The problem is that servers have a high energy consumption even if they are idle. The research works of the SEPIA team at IRIT focuses on energy-efficient cloud infrastructures scheduling.
In this master thesis we aim to study the dynamic adaptation of a datacenter in order to improve energy efficiency. The main focus will be to improve the workload scheduling and hardware adaptation.
The following steps will be tackled by the student:
-integrating highly heterogeneous datacenter with classical processors and GPUs
-using green leverages like DVFS, migrations...
-considering multiple simultaneous and independant workloads
During this intership the student will use and extend the internal simulator BMLSim (developed in Python in collaboration with AVALON team at LIP).
Required skills are: scheduling, performance evaluation, distributed systems
URL sujet détaillé : :

Remarques : Co-encadrement : Georges Da Costa et Laurent Lefèvre



SM207-62 ECM in the NFS context  
Admin  
Encadrant : Laurent IMBERT
Labo/Organisme : LIRMM, ECo group
URL : https://www.lirmm.fr/eco/
Ville : Montpellier

Description  

Public-key cryptography has been a key ingredient in the deployment of e-commerce, for securing the private life of individuals and for protecting industrial and governmental secrets. Despite numerous advances in the field, the protocols from the first generation, such as RSA, are still widely used. Assessing the theoretical and practical difficulty of number theoretic questions which constitute the bedrock of these protocols, such as integer factorization or the finite field discrete logarithm problem is therefore still of utmost importance.

The major tool to gauge the hardness of these problems is the Number Field Sieve (NFS) algorithm. One of its phases consists in checking whether some "numbers" can be broken into small factors. In particular, the cofactorization step represents an important, and time consuming operation: given a medium size composite integer, the goal is to compute its factors if they are all less than a given bound, or decide rapidly whether to skip that integer if the operation takes too much time. The main algorithm for this routine is the ECM method based on elliptic curves.

The goals of this internship is to study the ECM algorithm and to propose algorithmic improvements in the very specific context of NFS. The results will be integrated in the CADO-NFS software.

URL sujet détaillé : :

Remarques : Co-encadrant : Cyril Bouvier



SM207-63 Floating-point expansions algorithms with certified error bounds  
Admin  
Encadrant : Jean-michel MULLER
Labo/Organisme : LIP, ENS Lyon
URL : http://homepages.laas.fr/mmjoldes/campary/
Ville : Lyon

Description  

Many numerical problems require higher precision than the one offered by conventional floating-point (FP) formats, either because the problem is numerically delicate (needs very large precision), or the processor used natively supports only the single-precision format. One solution is to use multi-precision libraries such as GNU-MPFR (http://www.mpfr.org), or it's extension to interval arithmetic GNU-MPFI (http://perso.ens-lyon.fr/nathalie.revol/software.html). Both of these use the multiple-digit representation, meaning that numbers are represented as a sequence
of possibly high-radix digits coupled with a single exponent.
This alternative proves to be quite heavy in some cases when a precision of a few hundred bits is sufficient and we have strong performance requirements. Examples of such problems can be found in domains like dynamical systems, ranging from the study of the mathematical properties of classical dynamical systems such as Henon attractor, to celestial mechanics for the study of the stability of the solar system. Other areas include numerically ill conditioned optimization problems in computational geometry, quantum information or quantum physics, etc.
More than often these problems can also benefit from the use of high performance computing and accelerators such as NVIDIA's GPUs (Graphics Processing Units). Unfortunately none of these aforementioned libraries is ported on the GPU and they proved not to be a natural fit for it, due to their memory heavy nature.
An alternative is to use libraries based on the multiple-term representation. This approach represents numbers as the unevaluated sum of several standard FP numbers, also known as FP expansions, which offers the simplicity of using directly available and highly optimized hardware implemented FP operations. This makes most multiple-term algorithms straightforwardly portable to highly parallel architectures, such as GPUs. Libraries that use this approach include Bailey's well known QD library (http://crd-legacy.lbl.gov/~dhbailey/mpdist/), that supports double-double (DD) and quad-double (QD) precision, i.e., numbers are represented as the unevaluated sum of 2 or 4 double precision numbers. A newer alternative is CAMPARY (http://homepages.laas.fr/mmjoldes/campary/), a library that supports arbitrary precision and can use as underlying FP format both single and double-precision numbers. The aim of this internship is to help develop an interval arithmetic module for CAMPARY.

The objectives of this internship are:
1. Study and understand the algorithms for basic operations using FP expansions implemented in CAMPARY;
2. Analyze aspects related to interval arithmetic and decide on the best approach to be implement (mid-radix vs. endpoints representation), keeping in mind memory usage and performance requirements;
3. Design and implement simple and efficient algorithms for performing basic operations using multiple-precision interval arithmetic.
4. This new module will be applied on problems on dynamical systems, in collaboration with Prof. Warwick Tucker and CAPA team http://www2.math.uu.se/ ̃warwick/CAPA at University of Uppsala, Sweden.

This internship can be followed by a PhD thesis.
URL sujet détaillé : http://perso.ens-lyon.fr/valentina.popescu/IntervalLib.pdf

Remarques : Advisors:
Mioara Joldes, MAC team, LAAS-CNRS, Toulouse
email: joldes.fr
Jean-Michel Muller, AriC team, LIP, ENS Lyon
email: jean-michel.muller-lyon.fr
Valentina Popescu, AriC team, LIP, ENS Lyon
email: valentina.popescu-lyon.fr



SM207-64 Geometric Construction of Wasserstein Barycenters  
Admin  
Encadrant : Nicolas BONNEEL
Labo/Organisme : LIRIS
URL : http://liris.cnrs.fr/~nbonneel/
Ville : Villeurbanne

Description  

Optimal transport seeks to reshape one probability distribution toward another. Among numerous applications is the construction of displacement interpolation: a probability distributions which is "in-between" the two input distributions. This is obtained by partially moving mass.
In the case where one distribution is absolutely continuous (with density) and the other is discrete (a weighted sum of Diracs), geometric constructions based on Laguerre's (or power) diagrams have been developped.

The optimal transport theory has led to the concept of Wasserstein barycenters, which generalizes displacement interpolation to the case of more than two input distributions.

The goal of this internship is to study how the geometric construction of displacement interpolation can be extended to Wasserstein barycenters.

More details at: http://liris.cnrs.fr/~nbonneel/project_transport.pdf
URL sujet détaillé : http://liris.cnrs.fr/~nbonneel/project_transport.pdf

Remarques : Co-advised by Nicolas Bonneel (CNRS / LIRIS) and Julie Digne (CNRS / LIRIS), and in collaboration with Bruno Lévy (INRIA / LORIA) and Jean-Marie Mirebeau (CNRS / Orsay).
Internship held at Campus La Doua (Lyon 1).



SM207-65 Captured 3d animation super-resolution  
Admin  
Encadrant : Nicolas BONNEEL
Labo/Organisme : LIRIS
URL : http://liris.cnrs.fr/~nbonneel/
Ville : Villeurbanne

Description  

3d scanning techniques often offer either high spatial resolution but low temporal resolution (e.g., LIDAR scanners which take seconds to minutes per object) or low spatial resolution with high temporal resolution (e.g., a Kinect operates in realtime).
Also, low-temporal resolution means distortions when used on moving objects.

The goal of this internship is to recover point-cloud animations from the combination of both kinds of sources. This amounts to removing distortions from the low-temporal resolution source while transfering the recovered details to the low-spatial resolution source.
URL sujet détaillé : http://liris.cnrs.fr/~nbonneel/stageM2.htm

Remarques : Co-advised by Nicolas Bonneel (CNRS / LIRIS) and Julie Digne (CNRS / LIRIS).

The internship will be held at Campus La Doua (Lyon 1).



SM207-66 Branch prediction on GPU architectures  
Admin  
Encadrant : Sylvain COLLANGE
Labo/Organisme : Inria / IRISA
URL : https://team.inria.fr/pacap/members/sylvain-collange/
Ville : Rennes

Description  

Les processeurs graphiques (GPU) maintiennent un grand nombre de threads actifs simultanément, chacun exécutant le même programme
sur des données distinctes. Les GPU emploient un modèle d'exécution SIMT (Single-Instruction Multi-Threading) qui consiste à synchroniser l'exécution de plusieurs threads pour qu'ils exécutent la même instruction au même moment. La lecture, le décodage des instructions et la logique de contrôle sont ainsi factorisés entre plusieurs threads. Ce mode d'exécution est favorable au débit d'exécution, au détriment de la latence.

L'objectif de ce stage est de généraliser la prédiction de branchements aux architectures GPU afin de leur permettre d'exécuter plus efficacement du code faiblement parallèle. L'exécution en mode SIMT soulève de nouvelles problématiques par rapport à la prédiction de branchement traditionelle. Dans le contexte classique, un branchement est soit pris, soit non-pris. En SIMT, un branchement peut a) être pris par tous les threads, b) n'être
pris par aucun thread, ou c) être divergent, c'est-à-dire pris par certains threads mais pas par d'autres. Dans ce dernier cas, il faudra parcourir les deux directions du branchement : la décision du prédicteur n'affectera que l'ordre dans lequel les chemins sont exécutés.
URL sujet détaillé : http://www.irisa.fr/alf/downloads/collange/stage_m2_2017_gpubranchpred.pdf

Remarques :



SM207-67 Ground-truth specular intrinsic decompositions  
Admin  
Encadrant : Nicolas BONNEEL
Labo/Organisme : LIRIS
URL : http://liris.cnrs.fr/~nbonneel/
Ville : Villeurbanne

Description  

Given an input photograph I, the intrinsic decomposition problem consists in finding a decomposition into a shading layer S and a reflectance layer R such that I = S*R.
This problem has led to numerous algorithms. In this context, ground truth decompositions for which the decomposition is exactly known are necessary:
- for algorithms based on machine learning
- to validate all algorithms.
However, very few ground truth databases exist, and none of them are realistic. Some databases are based on physical objects which are covered in white paint to obtain the shading layer, other databases rely on synthetic 3D renderings for which the reflectance layer is easily obtained.

In all these databases, one reason for the lack of realism is the lack of specularities. In fact, the intrinsic decomposition problem only makes sense for perfectly diffuse objects, which inherently limits the realism of processed scenes.

This internship will consist in building a more flexible model which includes a specular layer P, such that I = S*R + P. In this context, the student will need to find a way to obtain the layers S, R and P from 3d physically-based renderers given 3d objects of various (specular) materials.
URL sujet détaillé : :

Remarques : Co-advised by Nicolas Bonneel (CNRS / LIRIS) and Julie Digne (CNRS / LIRIS).

The internship will be held at Campus La Doua (Lyon 1). This internship does not offer funding and only accepts students already funded by ENS (or by other means).



SM207-68 Information theory  
Admin  
Encadrant : Omar FAWZI
Labo/Organisme : LIP
URL : http://perso.ens-lyon.fr/omar.fawzi/
Ville : Lyon

Description  

Information theory studies the fundamental limit of basic information processing tasks such as compression or channel coding over various kinds of channels and constraints. These problems can all be seen as an optimization over encoding and decoding functions with specific properties.

In traditional information theory, one assumes some structure on the resource, typically, a memoryless channel or iid source, and tries to determine an entropic quantity that determines the optimal asymptotic rate.

The objective of this internship would be to look at the optimization problem from an algorithmic and complexity theoretic point of view. How hard is this optimization problem to solve or to approximate? Such a study was initiated in https://arxiv.org/abs/1508.04095 but only for one formulation of channel coding. There are many more information theoretic tasks for which such a treatment could be very fruitful, for example:
- Quantum channels (sending classical or quantum information)
- Channel coding in a different regime (e.g., very small error probability)
- Network problems (multiple access channel, broadcast channel etc...)

The objective of the internship would be to tackle one such problem, depending on the students' interests.

Prerequisites: Probability, Information theory, Optimization (linear programming, approximation algorithms).

URL sujet détaillé : :

Remarques :



SM207-69 Rule-based meta-modelling  
Admin  
Encadrant : Russ HARMER
Labo/Organisme : LIP
URL : http://perso.ens-lyon.fr/russell.harmer/
Ville : Lyon

Description  

Rule-based meta-modelling is a graph-based generalization of set-based approaches (e.g. UML, OWL) to modelling in general. In this internship, we are specifically concerned with conceptual and practical tools for the modelling of biological systems -- cellular signalling networks -- and, in particular, with the development of an infrastructure for maintaining multiple models of a given network, e.g. for different species (human vs mouse, etc) or in the face of apparent contradictions in the biological literature (variant hypotheses). This infrastructure will enable the expression of vital provenance meta-data -- e.g. this interaction in humans is hypothesized because it has been observed in mice and the proteins involved are conserved (orthologous) in humans; or similar paralogy hypotheses within a species -- that documents knowledge transfer and the induced correspondences between models; and provide support for the gradual convergence of variant hypotheses to a single consensus model for a given species.
URL sujet détaillé : :

Remarques :



SM207-70 String graphs on surfaces and the shortcut problem  
Admin  
Encadrant : Francis Et Arnaud LAZARUS ET DE MESMAY
Labo/Organisme : GIPSA-Lab, UMR CNRS 5216
URL : http://www.gipsa-lab.fr/~arnaud.demesmay/ and http
Ville : Grenoble

Description  

String graphs are graphs that can be realized as intersection graphs of curves in the plane: a graph G = (V, E) is a string graph if there exists a family of |V | curves (strings) drawn in R2 such that no three strings intersect at a single point and such that the strings represent G, i.e., G is isomorphic to the graph having a vertex for each curve and an edge for each intersecting pair of curves. The study of these graphs originates from practical problems in VLSI design [7], and they form both a natural and a mysterious class of graphs. For a while, it was unknown whether recognizing a string graph is decidable. The key challenge to design an algorithm for recognition is to establish a bound on the number of intersections of the pairs of strings representing a string graph.

A natural generalization of string graphs is to consider string graphs on surfaces, where the realizations involve curves drawn on a fixed surface. Here again, the issue is to bound the number of intersections of strings representing a graph on a surface. The object of the internship is to make progress on this question.

More details and references in the detailed project at the URL below.



URL sujet détaillé : http://www.gipsa-lab.fr/~francis.lazarus/Stages/Intern_M2_ENS-17-A.pdf

Remarques :



SM207-71 Irreducible triangulations  
Admin  
Encadrant : Francis Et Arnaud LAZARUS ET DE MESMAY
Labo/Organisme : GIPSA-Lab, UMR CNRS 5216
URL : http://www.gipsa-lab.fr/~arnaud.demesmay/ and http
Ville : Grenoble

Description  

A triangulated surface is irreducible if any edge contraction leads to a degenerate triangulation, or equivalently if every edge belongs to at least one 3-cycle which is not the boundary of an incident triangle. Properties on irreducible triangulations sometimes extend to the whole set of triangulations. This is e.g. the case for the existence of a non-contractible separating cycle.
Barnette and Edelson proved that each topological surface has a finite number of pairwise non-isomorphic irreducible triangulations. In general the best we can say is that the number of vertices of the genus is at most g -4 This bound implies that there are (g)^{O(g)} triangulations. This is a loose bound and the aim is to obtain a tighter bound by a topological approach.

A pants decomposition of a surface is a maximal family of simple non-contractible curves that are pairwise disjoint and non-homotopic. A pair of pants is a three-holed sphere, and a pants decomposition cuts a triangulated surface into a collection of g -2 pairs of pants.
The approach relies on such decompositions to enumerate irreducible triangulations.

More details and references in the detailed project at the URL below.
URL sujet détaillé : http://www.gipsa-lab.fr/~francis.lazarus/Stages/Intern_M2_ENS-17-B.pdf

Remarques :



SM207-72 Homotopy techniques for determinantal systems  
Admin  
Encadrant : Eric SCHOST
Labo/Organisme : Cheriton School of Computer Science, University of Waterloo
URL : https://cs.uwaterloo.ca/~eschost/
Ville : Waterloo

Description  

Solving determinantal polynomial systems (that is, systems whose
equations are obtained as minors of polynomial matrices) is a
recurring question in domains such as optimization or real algebraic
geometry. Results known as of now are not entirely satisfying; for
instance, there is no known algorithm that would solve such systems
with a complexity depending on the expected number of solutions.

Homotopy continuation techniques rely on following a deformation
between the system one has to solve and another system, with a similar
combinatorial structure, but whose solutions are easy to describe.
They have proven to be very successful in both numerical and symbolic
contexts, for several families of systems (homogeneous,
multi-homogeneous, polyhedral). The goal of this internship is to
study how these techniques could be applied in the context of
determinantal systems, and resolve the issue above.
URL sujet détaillé : :

Remarques :



SM207-73 Bit complexity of algorithms for isolated points  
Admin  
Encadrant : Eric SCHOST
Labo/Organisme : Cheriton School of Computer Science, University of Waterloo
URL : https://cs.uwaterloo.ca/~eschost
Ville : Waterloo

Description  

Consider a system of equations =dots=f_s=0 a solution
this system. A classical question is to determine the {em
multiplicity} of these equations at  beyond the multiplicity, one
is often interested in determining the local structure of the system
,dots,f_s For instance, if =(y-x^2)(y+x+1)
=y and =(0,0) the multiplicity is =2 and 100 24 25 29 44 46 100 110 118 200 201 2591,x) a
basis of the local algebra.

There exist algorithms that answer this question; their behavior is
well understood in an {em algebraic} model, where all base field
operations have the same cost. Over a field such the
analysis of the boolean complexity of such algorithms is somehow less
accurate. The goal of this internship is to clarify this analysis, and
to develop a {em modular algorithm}, that proceeds through reduction
modulo a well-chosen prime.
URL sujet détaillé : :

Remarques :



SM207-74 Performance Study of Public Clouds  
Admin  
Encadrant : Lucas NUSSBAUM
Labo/Organisme : LORIA
URL : http://members.loria.fr/lnussbaum
Ville : Nancy

Description  

The goal of this internship is to design new methods for the
performance evaluation of public clouds offerings, robust to adverse strategies that
might be deployed by some cloud providers.
URL sujet détaillé : https://members.loria.fr/lnussbaum/2016/clouds-eval.pdf

Remarques : internship in collaboration with a french startup (CloudScreener) which will provide access to many public clouds.



SM207-75 Big Data Performance Emulation in Distem  
Admin  
Encadrant : Lucas NUSSBAUM
Labo/Organisme : LORIA
URL : http://members.loria.fr/lnussbaum
Ville : Nancy

Description  

The goal of this project is to extend the Distem emulator in order to
support experimentation on Software-Defined Storage solutions.
URL sujet détaillé : https://members.loria.fr/lnussbaum/2016/distem-io.pdf

Remarques :



SM207-76 Designing experimentation tools for Software Defined Networking  
Admin  
Encadrant : Lucas NUSSBAUM
Labo/Organisme : LORIA
URL : http://members.loria.fr/lnussbaum
Ville : Nancy

Description  

The goal of this project is to design extensions to Grid'5000 and Distem to
support experimentation on SDN.
URL sujet détaillé : https://members.loria.fr/lnussbaum/2016/xp-sdn.pdf

Remarques :



SM207-77 Deep learning for autonomous curious agents  
Admin  
Encadrant : Mathieu LEFORT
Labo/Organisme : LIRIS
URL : http://liris.cnrs.fr/mathieu.lefort/
Ville : Lyon

Description  

This internship is related to (strong) artificial intelligence and machine learning. It aims to combine deep learning with artificial curiosity to obtain autonomous agents (robots, information systems, ...) that are able to learn and act in unknown and changing environments. Deep learning algorithms, based on stochastic optimization of non linear functions regression, provide models with strong generalization abilities. However, they suffer from catastrophic forgetting when the relation to learn is ill posed or non stationary. Artificial curiosity is a meta-learning algorithm that incrementally split the relation to learn in area of increasing learning complexity. It thus provides a quicker learning by focusing on interesting areas first.
In this internship, we target the following points:
- characterization of deep learning in term of curiosity interest
- use of artificial curiosity to prevent catastrophic forgetting
- build up learning in one area to bootstrap/combine learning in other adjacent areas (depending on the timing)


URL sujet détaillé : http://liris.cnrs.fr/mathieu.lefort/sujet_ENS_2017.pdf

Remarques : Co-encadrement: Frédéric Armetta (SMA, LIRIS)



SM207-78 Linear graph rewriting for Boolean logic  
Admin  
Encadrant : Anupam DAS
Labo/Organisme : LIP - ENS Lyon
URL : http://www.ens-lyon.fr/LIP/
Ville : Lyon

Description  

Linear graph rewriting for Boolean logic.


This project is about 'reducing' Boolean expressions in a correct way, simulating logical reasoning. For example:

x AND (y OR z) -> (x AND y) OR (x AND z) (*)

Given a set of such reductions, one can chain together various instances to construct 'proofs'. In particular, one can construct sets of such reductions that are 'complete', i.e. from which we can prove every correct reduction.

A striking feature of all known complete sets is that they all involve *duplication of variables*. For example, in the above reduction the variable x is duplicated. What happens when we do not allow such behaviour? For example:

x AND (y OR z) -> (x AND y) OR z

This rule lies at the heart of Girard's 'Linear Logic', which successfully demonstrates the advantages of considering duplication-free fragments of Boolean logic. In fact this 'linear' fragment of Boolean logic is rich enough to encode the entire logic: it is already coNP-complete. Hence arrives our motivating question:

(Q) Can we construct reduction systems that are correct and complete for *linear* Boolean logic?

In particular, this requires us to remain in the world of linear Boolean expressions, for instance rejecting (*) and even intermediate non-linearity, e.g.:

x AND (y OR z) -> (x AND y) OR (x AND z) -> (x AND y) OR z

A complete linear system, unless coNP = NP, must admit reductions that are *exponentially long* but only *linearly wide*, a property consistent with but thusfar unobserved in proof complexity. There would also be far-reaching implications on the space complexity of various well-known proof systems.

In this project we propose to work with certain graphs extracted from Boolean expressions, called 'cographs'. The world of graphs is far more general than the world of logical expressions, *strictly extending* the class of Boolean functions, and so exhibits far richer and more expressive reduction behaviour. We believe that this setting admits reduction systems with the improved complexity properties that we desire.

Inspired by recent work, we propose to develop these ideas as follows:

* Develop a comprehensive framework for (co)graphs that models Boolean logic.
* Construct complete reduction systems based on (co)graphs.
* Obtain *separation results* distinguishing the world of graphs from that of Boolean expressions.

The first stages of this work were carried out by an L3 intern, Cameron Calk, last year and was very successful; we expect to soon publish a paper including much of that work. As a result, we are now in a good position to direct an M2 intern towards the fruitful directions coming out of this project.


Useful references

1. Rewriting with linear inferences in propositional logic. Anupam Das. http://drops.dagstuhl.de/opus/volltexte/2013/4060/
2. On linear rewriting systems for Boolean logi and some applications to proof theory. Anupam Das and Lutz Stra=DFburger. https://arxiv.org/abs/1610.08772
3. A graph theoretic extension of Boolean logic. Cameron Calk. L3 internship report, 2016. http://www.anupamdas.com/graph-bool.pdf
URL sujet détaillé : http://www.anupamdas.com/linear-rewriting.pdf

Remarques : Advisor:
Anupam Das
http://www.anupamdas.com/

Co-advisor:
Olivier Laurent
https://perso.ens-lyon.fr/olivier.laurent/



SM207-79 Infering transport modes  
Admin  
Encadrant : Antoine BOUTET
Labo/Organisme : LIRIS or LAAS
URL : https://sites.google.com/site/antoineboutet/
Ville : Lyon or Toulouse

Description  

Smartphones now integrate plenty of censors recording your location or your moves for instance. Although these contextual information have greatly improved the quality of many services, the exploitation of these data rises important concerns about privacy.
Indeed, a collection of mobility traces for instance (a set of timestamped locations reflecting the user's moving activity) can reveal many sensitive information about its user such as home and work places, favorite restaurants, religious leaning, or the
individuals she met.

The goal of this work is to analyse data from the accelerometer and gyroscope in order to infer the transport mode of users in real time.
To achieve that, based on state-of-the-art approaches, a machine learning approach such as a Hidden Markov Model will be trained and evaluated on real data.
Once the most relevant model identified, we will investigate the capability to localize users based on a trained model with data from public transportation, as well as the capability to re-identify users based on move fingerprints.
URL sujet détaillé : :

Remarques :



SM207-80 Infering transport modes  
Admin  
Encadrant : Antoine BOUTET
Labo/Organisme : LIRIS or LAAS
URL : https://sites.google.com/site/antoineboutet/
Ville : Lyon or Toulouse

Description  

Smartphones now integrate plenty of sensors recording your location or your moves for instance. Although these contextual information have greatly improved the quality of many services, the exploitation of these data rises important concerns about privacy.
Indeed, a collection of mobility traces for instance (a set of timestamped locations reflecting the user's moving activity) can reveal many sensitive information about its user such as home and work places, favorite restaurants, religious leaning, or the
individuals she met.

The goal of this work is to analyse data from the accelerometer and gyroscope in order to infer the transport mode of users in real time.
To achieve that, based on state-of-the-art approaches, a machine learning approach such as a Hidden Markov Model will be trained and evaluated on real data.
Once the most relevant model identified, we will investigate the capability to localize users based on a trained model with data from public transportation, as well as the capability to re-identify users based on move fingerprints.
URL sujet détaillé : :

Remarques :



SM207-81 Intersrf++  
Admin  
Encadrant : Dave RITCHIE
Labo/Organisme : INRIA
URL : https://members.loria.fr/DRitchie/ritchie.html
Ville : Nancy

Description  

The main objective is to develop a new program to calculate and visualise 3D protein interfaces using the CGAL computational geometry library and OpenGL 3D graphics. An early prototype was developed in C but cannot be interfaced with modern computational geometry library nor with recent protein modelisation software. Ultimately, we want to use the developed program to be able to compare the similarities and differences in protein complex interfaces across related families of proteins, and to measure how interfaces change during molecular dynamics simulations of protein flexibility.
URL sujet détaillé : http://www.loria.fr/equipes/vegas/sujets-master.pdf

Remarques : This project is proposed through a collaboration between the Capsid and Vegas research teams:
Capsid: Computational Algorithms for Protein Structures and Interactions.
Vegas: Computational geometry.



SM207-82 Root solver using subdivision and Fast Fourier Transform  
Admin  
Encadrant : Guillaume MOROZ
Labo/Organisme : INRIA/LORIA
URL : https://members.loria.fr/GMoroz/
Ville : Nancy

Description  

In scientific computation, finding the roots of polynomial equations is a fundamental problem arising in robotics or visualization for example. Bisection is a standard numerical method to solve this problem [1,=A72.1]. On the other hand, it requires to evaluate the input polynomials at each bisection step, and for a high degree polynomial p, evaluating p can be costly. Approaches based on Fast Fourier Transform can be used to evaluate a polynomial on several point for the cost of one evaluation [2,=A78.2, Cor.10.8]. These approaches have never been used in numerical root-finding methods. The goal of this internship is to use multipoint evaluation approaches to improve significantly root-finding methods for univariate and bivariate polynomial equations.
URL sujet détaillé : https://members.loria.fr/MPouget/files/web_files/sujet-subdivision.pdf

Remarques : Co-encadrement avec Marc Pouget



SM207-83 Édition rapide de programmes dirigée par la performance  
Admin  
Encadrant : Florent BOUCHEZ TICHADOU
Labo/Organisme : LIG (Université Grenoble Alpes)
URL : https://team.inria.fr/corse
Ville : Grenoble

Description  

La génération de code binaire efficace est redevenu un problème scientifique difficile à cause
d'une part de la complexité croissante des architectures de calcul et d'autre part du niveau d'abstrac-
tion élevé des langages de programmation.
En pratique, le nombre d'étapes entre la rédaction d'un programme et son optimisation est
très grand : rédaction du programme, compilation, déploiement, exécution sur un jeu de données,
mesures d'efficacité, etc. ce qui nécessite des développeurs expérimentés et beaucoup de temps de
développement.

La plupart des outils de compilation dédiés à la performance sont écrit pour un public d'experts (par
exemple le profilage), et peu d'outils travaillent directement sur le code au moment de sa rédaction,
au delà de la simple complétion " intelligente " proposée par les IDEs.

Le sujet de ce stage sera alors d'étudier la possibilité de créer des outils permettant de réaliser
la compilation et d'étudier la performance d'un code au moment de la rédaction du programme
(" edit-time "). Nous partons en effet du postulat que plus une information pertinente est rapprochée
physiquement (visuellement) et temporellement (au moment de l'écriture) du code, plus faible sera
l'effort cognitif nécessaire au traitement de cette information, ce qui permet de gagner en efficacité
de développement, mais aussi d'agir directement sur les parties du programme non efficaces.
Il est attendu du candidat durant son stage,
en plus de l'état de l'art habituel, qu'il choisisse l'un des points suivants à étudier :

1. Quelles technologies de description de langage (lexer, parser) permettent de reconnaître un
langage dont le programme est en cours de rédaction ?

2. Comment modifier les technologies de compilation, qui travaillent habituellement avec un
code entièrement rédigé, pour qu'elles apportent en temps réel des informations sur la validité
d'un programme et des suggestions pour l'amélioration de la performance ? (vérification des
types, erreurs de syntaxe, analyse de code mort...).

3. Quelles technologies de compilation permettent de générer rapidement un code binaire
efficace par exemple pour un langage de type Javascript ?

4. Quels sont les critères de mesure de la qualité du code généré : efficacité, variabilité en
fonction du jeu de données, empreinte mémoire, vitesse de génération de code, etc.

URL sujet détaillé : https://dl.dropboxusercontent.com/u/6695281/2015-05-JavaScript-JIT-V3.pdf

Remarques : Le sujet détaillé en pdf représente un sujet de thèse complet dans lequel la totalité des points évoqués serait à travailler.



SM207-84 High-Speed Constant-Time Cryptographic Implementations  
Admin  
Encadrant : Gilles BARTHE
Labo/Organisme : IMDEA Software Institute
URL : http://software.imdea.org/~gbarthe
Ville : Pozuelo de Alarcon

Description  

Cryptographic libraries should achieve at least the following goals: time-and- space efficiency, functional correctness, protection against side-channel attacks, and provable security (in the style of modern cryptography). Each property requires specific skills and is already hard to achieve when taken in isolation. Furthermore, the guarantees delivered by existing libraries vary greatly according to the goals considered; while provable security is well understood and supported by rigorous mathematical analysis, neither functional correctness nor protection against side-channel attacks are supported by practical
methods. There are multiple issues, but one main challenge is that these guarantees must be established for highly optimized assembly implementations. The goal of this project is to develop practical methods for verifying the "cryptographic constant-time" methodology, which is used by practitioners to mitigate potential cache-based timing attacks.


The first objective of the project will be to develop an automated method for proving constant-time at the the assembly level. We will focus on a baseline policy, in which outputs are not publicly observable (although it is secure in some scenarios to leak control-flow information that is already contained in public outputs, there are multiple reasons to adhere to this simpler policy; in particular, it is widely used, and simpler to enforce). To this end, we will build on the methodology we recently proposed (Barthe et al: Verifying Constant-Time Implementations, Usenix Security, 2016). Depending on progress, thesecond objective of the project will be to extend the tool and
method to vectorized implementations on other platforms. A third, and complementary objective, will be to study under which conditions lower-compilation passes (for example from Register Transfer Language downwards) may preserve the constant-time property.
URL sujet détaillé : :

Remarques :



SM207-85 Vérification formelle performante pour la logique temporelle relationnelle sur domaines bornés   
Admin  
Encadrant : David CHEMOUIL
Labo/Organisme : ONERA/DTIM
URL : http://www.onera.fr/staff/david-chemouil/
Ville : Toulouse

Description  

Contribution to the definition of a formal specification language based upon a mixture of first-order logic (interpreted over bounded domains) and linear temporal logic. The contribution may range from foundational work to more "practical" work on automated verification techniques, or to the proposition of extensions to the logic (e.g. a timed extension).
URL sujet détaillé : http://chemouil.fr/foltl-stage-2017.pdf

Remarques : Co-encadrement avec Julien Brunel. Stage rémunéré.



SM207-86 Linéarisation de graphes de solutions pour l'échafaudage de génomes  
Admin  
Encadrant : Annie CHATEAU
Labo/Organisme : LIRMM
URL : http://www.lirmm.fr/~chateau
Ville : Montpellier

Description  

Contigs are relatively small pieces of genomic sequences produced by the assembly of sequencing data. During genome whole sequence production, the task performed by the scaffolding step is to determine how to place the contigs produced by assembly on the genome.
Ideally, the scaffolding have to produce the sequence of the contigs along each chromosome, using additional information. Formally, it is possible to extract from this information a set of relationships between the contigs, that may be inconsistent. We use here a model, based on a graph called the scaffold graph, which aims to take into account all these relationships,
weighted by a measure of confidence. In this model, the scaffold problem becomes an optimization problem that consists to find a covering of the scaffold graph by vertex-disjoint paths and cycles, which maximizes this measure of confidence. When contigs are allowed to appear several times in the final genome, paths and cycles become walks.
In order to translate a solution graph into sequences that occur in the target
genome, we have to reconstruct the walks that make up the solution graph. This,
however, may be ambiguous, since several walks could share a same set of edges. This information cannot be reconstructed from the graph alone.

The objective of the subject is to study the problem "Given a solution graph, how to safely produce a set of sequences?", from the complexity and approximation point of view, as well as parameterized complexity.
URL sujet détaillé : :

Remarques : Co-encadrement : Rodolphe Giroudeau, Mathias Weller



SM207-87 6 month  
Admin  
Encadrant : Adrien BOUSSEAU
Labo/Organisme : Inria
URL : http://www-sop.inria.fr/members/Adrien.Bousseau/
Ville : Sophia Antipolis

Description  

* Context and Research Goal *
Designers draw extensively to externalize their ideas and communicate with others. However, drawings are currently not directly interpretable by computers. To test their ideas against physical reality, designers have to create 3D models suitable for simulation and 3D printing. A long term ambition of our research group is to bring the power of 3D engineering tools to the creative phase of design by automatically estimating 3D models from drawings.

However, reconstructing 3D models from drawings is an ill-posed problem: a point in the drawing can lie anywhere in depth. In addition, line drawings are often drawn quickly and do not represent a perfect projection of a 3D object. We thus need additional constraints on the solution to reduce ambiguity and correct for drawing inaccuracy.

* Approach *
While line drawing reconstruction remains an open problem, several methods have been proposed for specific shapes (see [1] for polyhedrons) and drawing techniques (see our work [2] that exploits a technique called cross-sections). The main idea behind these approaches is to impose geometric constraints between the lines in the drawing. For instance, two lines that are parallel in the drawing are constrained to be parallel in 3D. However, existing methods often rely on heuristics to detect these constraints, such as thresholds to identify parallel lines. While these heuristics work well on simple examples, they are not sufficiently robust to handle real-world design drawings.

The goal of this internship is to design and implement a novel optimization method capable of jointly identifying constraints in a drawing and reconstructing the corresponding 3D shape. To do so, we need to consider a number of candidate constraints in the drawing (parallelism, orthogonality, symmetry) and associate each constraint with a binary variable that indicates if the constraint is active. These additional discrete variables make the problem a so-called Mixed-Integer formulation, which is NP-hard since finding the optimal solution would require testing all potential combinations of constraints. Instead, we need to devise efficient strategies to only evaluate a subset of high-quality configurations. One potential approach will be to use the existing heuristics to compute a probability distribution on the set of binary variables, and then rely on stochastic optimization such as Markov Chain Monte Carlo to evaluate the most probable constraint configurations. Other mixed-integer optimization strategies, such as the =93branch-and-bound=94 algorithm, may also be considered.
Finally, a long term goal is to leverage modern machine learning techniques to predict the probability that various constraints apply.

* References *
[1] H. Lipson and M. Shpitalni
Optimization-based reconstruction of a 3d object from a single freehand line drawing Computer-Aided Design 28, 651=96663. 1996
http://dl.acm.org/citation.cfm?id=1281556

[2] Baoxuan Xu, William Chang, Alla Sheffer, Adrien Bousseau, James McCrae, Karan Singh
True2Form: 3D Curve Networks from 2D Sketches via Selective Regularization
ACM Transactions on Graphics (Proc. SIGGRAPH) 2014
http://www.cs.ubc.ca/labs/imager/tr/2014/True2Form/index.htm

URL sujet détaillé : https://team.inria.fr/graphdeco/files/2016/10/drawing_optimization.pdf

Remarques : The internship will take place at Inria Sophia Antipolis, on the beautiful French riviera. The research will be conducted in the GraphDeco group (https://team.inria.fr/graphdeco/). The group does research on image synthesis and computer-aided design.

Inria will provide a monthly stipend of 1100 euros for EU citizen and 400 euros for non-EU.

This internship may be extended to a PhD.



SM207-88 A machine learning kernel for heterogenous architectures  
Admin  
Encadrant : Christophe CÉRIN
Labo/Organisme : LIPN UMR CNRS 7030
URL : http://lipn.univ-paris13.fr/bigdata/
Ville : Villetaneuse

Description  

Combining the logic blocks and interconnects of traditional FPGAs (Field-Programmable Gate Arrays) with embedded microprocessors and related peripherals to form a heterogenous architecture is a reality (first observation). At the same time, the field of machine learning is impacted by new parallel programming paradigms (second observation). Also, a notebook is a web-based interactive computational environment used to create documents which includes support for interactive data visualization, flexible and embeddable interpreters to load into the user's projects, as well as tools for parallel computing (third observation).

Goal: determine how to exploit heterogeneous architecture to build notebooks that exploit efficient machine learning kernels.

Workplan:
- Identify the state of the art work on heterogeneous architecture (FPGA...) and parallel frameworks for machine learning
- Focus on 2 identified basic blocks for machine learning and envision their implementation on heterogeneous architectures
- Integrate the programmed basic blocks into a machine learning algorithm
- Experiment with Xlink and Altera/Intel boards

Skills/Knowledge/Competencies:
(we do not require an expert in all of the mentioned areas-- some competencies will be acquired as the project progresses)
- Big data and machine learning background
- Computer architecture background
- Parallel computing background
- Experience with experimental evaluation
- Understanding of programming / logic design for computer architectures
- Ability to communicate well

URL sujet détaillé : http://lipn.univ-paris13.fr/~cerin/FPGA.pdf

Remarques : Mustapha Lebbah (Mustapha.Lebbah.univ-paris13.fr)
Jean-Luc Gaudiot (gaudiot.edu)

Legal compensation
Accomodation in Paris (subject to conditions)



SM207-89 Matching algorithms for dynamically changing bipartite graphs  
Admin  
Encadrant : Bora UÇAR
Labo/Organisme : LIP
URL : http://www.ens-lyon.fr/LIP/
Ville : Lyon

Description  

A matching in a graph is a subset of edges no two sharing a common vertex. A perfect matching is a matching where all vertices are on a matching edge. Given a bipartite graph with edge weights, the bottleneck value of a matching is defined as the minimum weight of an edge in that matching. The maximum bottleneck perfect matching (MBPM) problem asks for a perfect matching having the maximum bottleneck value. The MBPM problem is efficiently solvable in polynomial time for a given bipartite graph.

This internship is concerned with dynamically changing bipartite graphs. Suppose we have an edge weighted bipartite graph and a maximum bottleneck perfect matching, and suppose that the edge weights undergo slight changes. How fast can we compute a new maximum bottleneck perfect matching under the new edge weights? What about the next one, and the next say k of them, where k is a much smaller than the number of vertices. The internship will seek answers to these questions. The intern will help in designing, analyzing, and potentially implementing algorithms.

The internship requires theoretical and algorithmic background; in particular graph theory and algorithms, amortized analysis of algorithms, and probabilistic reasoning will likely be very useful.
URL sujet détaillé : :

Remarques :



SM207-90 Utilisation de prouveurs automatiques en Coq  
Admin  
Encadrant : Chantal KELLER
Labo/Organisme : LRI
URL : https://www.lri.fr/~keller
Ville : Orsay

Description  

SMTCoq is a Coq plugin that provide Coq users with new tactics that automatically solve Coq goals by safely calling external automatic theorem provers.

The goal of the internship is to increase the capabilities of these tactics by increasing their expressivity as well as their usability.
URL sujet détaillé : https://www.lri.fr/~keller/Documents-recherche/Propositions-stage/coq-automated-provers.pdf

Remarques : Pas de possibilité de rénumération



SM207-91 Calcul vérifiable pour Coq  
Admin  
Encadrant : Chantal KELLER
Labo/Organisme : LRI
URL : https://www.lri.fr/~keller
Ville : Orsay

Description  

Coq is a proof assistant based on the idea that computations are internal to the proof systems. As a result, powerful computation mechanisms are part of the trusting base of Coq, making it really huge.

The objective of the internship is to provide a new computation mechanism for Coq based on a cryptographic tool called Verifiable Computation. The idea is to delegate computation to an untrusted, external worker, and to check the result as a cryptographic evidence.

This internship does not require skills in Coq.
URL sujet détaillé : https://www.lri.fr/~keller/Documents-recherche/Propositions-stage/coq-verifiable-computation.pdf

Remarques : Pas de possibilité de rénumération



SM207-92 Segmentation semi-automatique de champs volumiques bivariés par surfaces fibrées  
Admin  
Encadrant : Julien TIERNY
Labo/Organisme : LIP6 - CNRS UPMC
URL : http://lip6.fr/Julien.Tierny
Ville : Paris

Description  

The purpose of this research internship is to propose, implement and evaluate an automatic algorithm for the segmentation of bivariate scalar fields defined on 3D tetrahedral meshes with fiber surfaces, for applications in interactive scientific data visualization and analysis.

The intern will build upon recent results in Topological Data Analysis for bivariate data obtained by the advisor of the internship regarding the efficient computation of Jacobi sets, Fiber Surfaces and Reeb spaces.

The designed algorithm will experimented and evaluated on 3D bivariate data coming from quantum chemistry, astrophysics and computational fluid dynamics simulations.
URL sujet détaillé : http://www-pequan.lip6.fr/~tierny/stuff/openPositions/internship2017.html

Remarques :



SM207-93 Etude et conception de mécanismes de contrôle pour la gestion de workflows autonomiques en environnement Cloud  
Admin  
Encadrant : Eric RUTTEN
Labo/Organisme : INRIA ou ENS de Lyon
URL : https://team.inria.fr/ctrl-a/fr/author/rutten/
Ville : Grenoble ou Lyon

Description  

voir le pdf ci-joint
URL sujet détaillé : http://graal.ens-lyon.fr/~ecaron/m2/Sujet_M2_WorkflowControl.pdf

Remarques : Co-encadrement Eric Rutten (CR Inria) et Eddy Caron (ENS de Lyon)



SM207-94 Graph recoloring  
Admin  
Encadrant : Louis ESPERET
Labo/Organisme : G-SCOP
URL : http://oc.inpg.fr/esperet
Ville : Grenoble

Description  

A (proper) k-coloring of a graph G is a coloring of the vertices of G with k colors, such that adjacent vertices receive distinct colors. Two k-colorings are said to be incident if they differ on exactly one vertex. A graph is k-recolorable if any k-coloring can be transformed into any other via a sequence of (incident) proper colorings.

The recoloring problem has been introduced in statistical physics, and people in this community are interested in minimizing the "distance" between two k-colorings in a k-colorable graph (having a polynomial, or even linear bound on this distance is very important).

Cereceda conjectured in 2007 that any (d+2)-coloring of a d-degenerate graph can be transformed into any other via a sequence of quadratic size. This conjecture is still open even for d=2.

The goal of the internship is two-fold:

- For planar graphs (that are 5-degenerate), we know that any 8-coloring can be transformed into any other via a polynomial sequence. We also know that there exist 6-colorings that cannot be transformed into any other. Prove the Cereceda's conjecture for 7 colors on planar graphs and close the gap between 6 and 8 will be a first objective.

- For chordal graphs (graphs without chordless cycles of length at least 4), Cereceda's conjecture has been proved in 2011. We also know that the transformation becomes linear if the number of colors is twice the degeneracy. Determining precisely for which value the diameter becomes linear is a central question for physicists who want to generate a coloring at random.


Keywords: Reconfiguration, graph coloring, planar graphs, chordal graphs.
URL sujet détaillé : :

Remarques : Possibilité de rémunération. Stage co-encadré par Nicolas Bousquet (G-SCOP)
https://liris.cnrs.fr/~nbousque/



SM207-95 Structure of even-hole-free graphs  
Admin  
Encadrant : Nicolas TROTIGNON
Labo/Organisme : LIP
URL : http://perso.ens-lyon.fr/nicolas.trotignon/indexFr.html
Ville : Lyon

Description  

Structure of even-hole-free graphs. Everything is explained in the file.
URL sujet détaillé : http://perso.ens-lyon.fr/nicolas.trotignon/sujet2016.pdf

Remarques : Co-encadrement par Stéphan Thomassé




Last modification : 2016-11-25 11:12:54 laurent.lefevre@ens-lyon.fr View source.