## Upcoming session: October 17th, 2017

**
Léo Perrin
** (SECRET)

**
Florian Omnès ** (UPMC, LJLL)

## Just another seminar?

The Junior Seminar (« séminaire des doctorants ») allows
**Inria PhD students / interns / post-docs to present their
work**. The talks are meant to be easily understandable, so
that **anyone can attend**.

The Junior Seminar is a good occasion to discover what the other teams are up to: if you ever wondered what's happening in other Inria's team this seminar is made for you.

## Where? When?

The seminar is usually scheduled every third Tuesday of the month, with a break during the summer. The seminar takes place in the Salle Jacques-Louis Lions in building C, usually at 2pm. Watch out for the posters!

## Format

The seminar is held in English to make sure everyone can attend. There are two 25-minute talks + two 5-minute sessions for questions after each talk. Coffee is provided, as well as snacks.

## I want to speak! I have a student who should speak!

Send us an email at semdoc@inria.fr, and we'll make sure you can give a talk :).

## Who are we?

**Currently in charge of the seminar:**
Léa
Boittin +
Patrik Daniel

**Formerly in charge of the seminar:**
Matteo Aletti+
Georgios
Bouloukakis+
Mathieu Feuillet
+ Emanuele Leoncini
+ Jonathan Protzenko
+ Elisa Schenone
+ Pauline Traynard
+ Jacques-Henri Jourdan
.

We're always looking for help, so if you want to help us find new victims and organize rehearsals, do contact us!

**PhD contacts at Inria:**

On this page you can find some useful links for PhD students at Inria.

Here are the archives of the Junior Seminar.

## June 13th, 2017

**
Thomas Boiveau
** (SERENA, ENPC (CERMICS))

(no slides ☹)

In computational mechanics, the imposition of boundary conditions is a major challenge, it is therefore crucial to use the right numerical tools to model in the best possible way a given boundary value problem. In this talk, we will introduce the Nitsche's method that is a very useful tool to impose boundary conditions in the framework of finite element. Nitsche's method is a way to impose weakly Dirichlet boundary conditions, this weak imposition allows us to extend the method to more complex problems such that, cut finite element, domain decomposition or fluid structure interaction.

**
Salah Eddine Saidi
** (AOSTE)

(no slides ☹)

The recent advancement in merging different technologies and engineering domains has led to the emergence of the field of Cyber-Physical Systems (CPS). Because of the heterogeneity of the involved components (multi-physics, sensors, actuators, embedded computers), CPS may feature very complex architectures and designs, ever raising the need for time, cost, and effort-effective approaches for building robust and reliable systems. Co-simulation has proven successful in responding to this need, and is therefore increasingly considered to be an indisputable step in design verification and validation. For complex CPS, experts of different engineering disciplines may be involved in the design process by developing models for different parts of the system. In a later stage, the developed models need to be integrated into one simulation environment and coupled together in order to perform simulation at the system level. The Functional Mock-up Interface (FMI) was developed with the goal of facilitating the co-simulation and the exchange of numerical models. One major challenge of co-simulation is the computing performance. In fact, integrating heterogeneous models into one environment usually results in a complex and heavy co-simulation which increases the demand of processing power. In this talk, I will give an overview of co-simulation of CPS, highlight some challenges for the parallelization of cosimulations, and present some results about the parallelization of closed-source co-simulations on multi-core processors.

## May 16th, 2017

**
Lélio Brun
** (PARKAS)

The compilation of block diagram languages like Lustre or Scade often use an intermediary language between the source data-flow code and the target imperative code. We recently implemented and verified a translation function in Coq from a simple intermediary language towards the Compcert-accepted Clight language. The intermediary language uses an idealized hierarchical memory representation, whereas Clight uses an intricate memory model rather close of the machine. Our proof of correctness must consequently tackle alignment, aliasing and padding. We use separation logic predicates developed in Compcert to solve those issues.

**
Georgios Bouloukakis
** (MiMove)

Systems deployed in mobile environments are typically characterized by intermittent connectivity and asynchronous sending/reception of data. To create effective mobile systems for such environments, it is essential to guarantee acceptable levels of timeliness between sending and receiving mobile users. To provide QoS guarantees in different application scenarios and contexts, it is necessary to model the system performance by incorporating the intermittent connectivity. Queueing Network Models (QNMs) offer a simple modeling environment, which can be used to represent various application scenarios, and provide accurate analytical solutions for performance metrics, such as system response time. In my talk, I will present you an analytical solution regarding the end-to-end response time between users sending and receiving data by modeling their intermittent connectivity with QNMs. We utilize the publish/subscribe middleware as the underlying communication infrastructure for mobile users. To represent the user's connections/disconnections, we model and solve analytically an ON/OFF queueing system by applying a mean value approach. Finally, we validate our model using simulations with real-world workload traces.

## April 18th, 2017

**
Jan Papez
** (ALPINES)

Many applications lead to solving (possibly very large) algebraic systems and this is often the most time-consuming part of the overall computation. In the talk we focus on the issues related to solution of algebraic problems stemming from numerical partial differential equations. In particular, we discuss the spatial distribution of the algebraic error and its comparison with the errors of other origins, the global and local error estimators, and stopping criteria for iterative algebraic solvers. The issues will be, on purpose, demonstrated using very simple model problems and the talk aims at providing the basic ideas and presenting the challenges, which are of general importance, related not only to numerical PDEs. We will do our best to avoid technical details and formulas, and to present the matter in a form comprehensible to a vast audience.

**
Cristian Maxim
** (AOSTE)

(no slides ☹)

The increased number of systems consisting of multiple interacting components imposes the evolution of timing analyses towards methods able to estimate the behavior of an entire system by aggregating timings bounds of its components. In the real-time domain these bounds are added to the worst case execution times (WCET) and the way they are obtained had always been subject to confusion and debate. In our work, we are using the probabilistic methods to determine the pWCET of a component starting from the execution time traces produced by the system. The correctness of our results is critical for the scheduling stage. In my presentation I will be explaining the notions of real-time systems, timing analysis, pWCET estimation and their use in daily life, concentrating on the avionics industry and its applications.

## March 14th, 2017

**
Jean-Karim Zinzindohoué
** (Prosecco)

(no slides ☹)

Implementing flawless, efficient and side-channel free cryptography is a notoriously hard problem. To tackle this issue we rely on F*, a functional ML-like proof oriented programming language. This language lets us mix concrete code and logical specifications about some code properties which it verifies statically at compile time. Using this technology, we present HACL*, a high assurance cryptographic library implemented and verified in F*. With formal methods we prove that the code is safe, functionally correct and free of certain classes of side-channels. The code is compiled to C through a proven safe extraction mechanism, yielding verified code which performance is on par with state-of-the-art C libraries.

**
Matteo Aletti
** (REO)

(no slides ☹)

The retina is a unique tissue in the human body since it is possible to observe non-invasively the microcirculation. In these tissues blood flow rate is regulated to satisfy specific metabolic needs or to accomodate for abrubt changes in the systemic pressure. The mechanism is based on fluid-structure interaction: arterioles vessels walls contain smooth muscle cells that contract or dilate to adapt the vessel diameter therefore changing its hidraulic resistance. A 3D model for this phenomenon will be presented with an application to a network of retinal vessels obtained from medical images.

## February 14th, 2017

**
Lara Trussardi
** (REO)

(no slides ☹)

In this talk I will present two different models for describing some socio-economic scenarios. The first model describes the dynamics of agents in a large market depending on the estimated asset value of a product and the rationality of the agents using a kinetic inhomogeneous Boltzmann-type equation. The second model describes the influence of knowledge and wealth in a society where the agents interact with the others through binary interactions. For both models numerical simulations has been implemented: for the first model the numerical simulations highlight the importance of the reliability of public information in the formation of bubbles and crashes. The use of Bollinger bands in the simulations shows how herding may lead to strong trends with low volatility of the asset prices, but eventually also to abrupt corrections. In the latter the kinetic code shows the possibility of cluster formation, using certain specific threshold and the formation of some interesting steady states.

**
Guillaume Terradot
** (ANTIQUE)

(no slides ☹)

Cells derive resources from their environments and use them to fuel the biosynthetic processes that determine cell growth. Depending on how responsive the biosynthetic processes are to the availability of intracellular resources, cells can build up different levels of resource storage. Here we use a recent mathematical model of the coarse-grained mechanisms that drive cellular growth to investigate the effects of cellular resource storage on growth. We show that, on the one hand, there is a cost associated with high levels of storage resulting from the loss of stored resources due to dilution. We further show that, on the other hand, high levels of storage can benefit cells in variable environments by increasing biomass production during transitions from one medium to another. Our results thus suggest that cells may face trade-offs in their maintenance of resource storage based on the frequency of environmental change.

## January 17th, 2017

**
Héctor Martínez Alonso
** (ALPAGE)

Multitask learning (MTL) is a general technique to train classifiers, where different datasets or 'tasks' are used together for training using a common loss function, in a way similar to many approaches to joint learning. MTL in neural networks has recently shown promising results for different tasks and architectures in natural language processing. Ideally, a MTL setup allows a network to learn from heterogeneous data sources and improve the quality of predictions by benefitting from the relations between the respective label inventories of the different tasks. In this work, we benchmark the response of a recent, successful architecture for linguistic sequence prediction (part of speech, named entities, etc) with regards to the choice of auxiliary task. Chiefly, we provide an empirical study on what data sources lend themselves to MTL, and provide an information-theoretical account of their properties.

**
Rafael Angarita
** (MiMove)

(no slides ☹)

Computer-mediated communication can be defined as any form of human communication achieved through computer technology. From its beginnings, it has been shaping the way humans interact with each other, and it has influenced many areas of society. There exist a plethora of communication services enabling computer-mediated social communication (e.g., Skype, Facebook Messenger, Telegram, WhatsApp, Twitter, Slack, etc.). Based on personal preferences, users may prefer a communication service rather than another. As a result, users sharing same interests may not be able to interact since they are using incompatible technologies. To tackle this interoperability barrier, we propose the Social Communication Bus, a middleware solution targeted to enable the interaction between heterogeneous communication services. More precisely, the contribution of this paper is threefold: (i), we propose a survey of the various forms of computer-mediated social communication, and we make an analogy with the computing communication paradigms; (ii), we revisit the service bus paradigm in the context of computer-mediated social interactions. We build on top of the extit{eXtensible Service Bus} (XSB), that supports interoperability across computing interaction paradigms, to provide a solution for computer-mediated social communication interoperability; and (iii), we present Social-MQ, an implementation of the Social Communication Bus that has been integrated into the AppCivist platform for participatory democracy.

## December 13th, 2016

**
Christèle Etchegaray
** (Orsay)

(no slides ☹)

Cell migration is a fundamental process involved in physiological processes such as embryogenesis, immune response, or tumor metastasis. Cells are active systems, and their internal activity involves a wide range of elements interacting on different time and space scales. Understanding the resulting behaviour is therefore a challenge. Our aim is therefore to construct a minimal trajectory model describing the multi-scale interactions involved in the process. In this talk, I will present a deterministic model of cell migration on a plane surface, where the cell domain is a non deformable disc. I will explain that structures involved in migration were shown to be also responsible for the reinforcement of cell polarisation at the molecular scale, leading to a self-reinforcement of the dynamics. Then, numerical simulations will show that several behaviours can be reached by the model. This work is in collaboration with Nicolas Meunier (MAP5, Univ. Paris Descartes) and Raphaël Voituriez (LJP, LPTMC, CNRS, UPMC).

**
Olivier Tissot
** (ALPINES)

Sparse linear systems of the form Ax=b where A is a n x n matrix arise in a lot of numerical problems. When n becomes very large it becomes necessary to use a supercomputer. However it is a very challenging issue to solve them in an efficient way on such machines. There exists a lot of methods for solving linear systems and the focus will be on Krylov methods and more precisely on the Conjugate Gradient: the method of choice when the matrix is symmetric positive definite. We will see how to redesign it in order to increase performances on parallel machines.

## November 15th, 2016

**
Markus Köppel
** (SERENA)

The talk is concerned with the dynamics of two-phase flow in a two-dimensional heterogeneous porous medium with randomly located interfaces. In the deterministic case discontinuities of the flux function occur due to the change of the material parameters. Based on the capillarity-free fractional flow formulation a hybrid Stochastic Galerkin method (HSG) for heterogeneous two-phase flow is presented. The classical polynomial chaos expansion is extended by a multi-element discretization. This yields a (weakly) coupled, deterministic and hyperbolic-elliptic system which allows for efficient parallelization.

**
Pierre Monmarché
** (Matherials (CERMICS))

For high-dimensional problems (protein folding, big data statistics, optimal path finding...), the use of deterministic algorithms may be prohibited by their numerical cost. In some cases, it is more efficient to try to solve the problem 'at random', more precisely to let the computer explore the configuration space according to a well-chosen random dynamic. In the basic versions of these so-called Monte-Carlo algorithms, the random process is memoryless : it never learns anything from what it has already seen, which is far from efficient. On the other hand, keeping a high-dimensional memory has a (possibly prohibitive) numerical cost. What can we do about this ?

## October 18th, 2016

**
Cécile Taing
** (Laboratoire Jacques-Louis Lions, UPMC)

(no slides ☹)

The interactions between individuals with a phenotypic variability usually lead to com- petition and selection of the fittest individuals. The goals of this work are to describe the asymptotic behaviour of the solution to a renewal type equation with a phenotypical structure and then to derive properties that illustrate the selection phenomena. As a first step, we begin with a simpler model by only considering the competition and disregard- ing the effects of mutations. The analysis is lead by the study of an eigenvalue problem, with eigenelements depending on the structuring variables of the model . Then we tackle the problem with mutations, which leads to the study of a constrained Hamilton-Jacobi equation.

**
Alexandre This
** (REO, Philips Research)

(no slides ☹)

The mitral valve can be subject to several pathologies resulting in blood regurgitation from the ventricle to the atrium. The proximal isovelocity surface area (PISA) method is widely used to assess the severity of the regurgitation. However, it relies on several assumptions on both fluid motion and morphology. We designed numerical simulations to assess the influence of breaking those assumptions on the PISA model. A simplified heart geometry was created and three different defects were introduced in the mitral valve. Four heart cycles were simulated using a fluid/structure interaction method. The simulated results were then compared with the estimation provided by the PISA method. In the simulation presented, the mitral defect shapes strongly affects the shape of the isovelocity surface and this results in important estimation error of clinically relevant quantities. Moreover, it was found that the aortic outflow influenced the regurgitation. These observations would justify the use of patient-specific models for clinicalevaluations. Further work includes the use of a more realistic patient geometry and the use of patient specific boundary conditions

## June 21st, 2016

**
Camilla Fiorini
** (LM UVSQ)

This seminar will be about sensitivity analysis for nonlinear hyperbolic equations. First we will introduce the general framework and talk about sensitivity analysis in wider terms; then, we will focus on the case of nonlinear hyperbolic equations, whose discontinuous solutions cannot be treated with the standard techniques.

**
Garvita Bajaj
** (MiMove)

(no slides ☹)

The last decade has seen a drastic increase in the number of smartphones being used by the people. These smartphones have sensing and computation capabilities which can be used to sense the physical world (activity, location, temperature, etc.) and the network world (other devices in network range). These sensing capabilities offer opportunities to develop new applications in several domains such as transportation, health monitoring, and environmental monitoring. Relying on the sensing capabilities of a large number of (un)known devices to measure phenomenon of common interest (e.g., pollution levels, traffic levels, etc.) is referred to as mobile crowdsensing (MCS). The developers of these mobile crowdsensing applications range from naive developers to academicians. To facilitate the development of these applications, several frameworks aimed at tackling specific challenges, have been proposed in the literature. However, to the best of knowledge, the problem of intelligent sensing task allocation to the participants of MCS applications, based on their resource levels, has not been tackled so far. In this task, I will introduce the concept of mobile crowdsensing, and the need for frameworks for development of MCS applications. I will begin with the motivation behind intelligent task allocation followed by our approach with preliminary results.

## May 17th, 2016

**
Katerina Tzompanaki
** (Telecom Paristech)

(no slides ☹)

With the increasing amount of available data and data transformations, typically specified by queries over the data, the need to understand them also increases.``Why are these medicine books in my sales report?'’ or ``Why are there not any database books?'' To answer such Why and Why-Not questions that typically arise both in the scientific and commercial world, data provenance plays a crucial role. While Why questions have been widely addressed in classical databases, this is surprisingly not the case for Why-Not questions that only recently attracted the interest of the research community.

**
Yi Yin
** (MAMBA)

(no slides ☹)

Tumor cellularity is an important tissue microstructural feature, which is useful for cancer diagnosis and cell number related treatment such as targeted cancer therapies. Diffusion-weighted MRI (DWI) that indicates the rates of water diffusion in tissue is used in medical imaging as it is thought to provide an indirect measure of tumor cellularity. Histopathological examination of tissues reveals the tissue microstructure, but is usually available as a small sample or after resection. How to quantitatively estimate the total tumor cell load is still a challenging work. In this study, we proposed a pipeline for tumor cell load estimation based on image processing techniques. The main pipeline steps include: 1) adaptive cell nuclei segmentation; 2) model based 3D cell density estimation; 3) correlation identification between the DW-MRI diffusion coefficient (D value) and the underlying tumor cellularity; 4) cell number calculation based on tumor D values and the identified correlation between diffusion and cellularity. The proposed cell segmentation algorithm performs detection with a very high accuracy (0.95) on selected tumor tissue samples. For a specific patient with NSCLC, the estimated total cell number of the tumor (6.5 cm in diameter) is 3.64×1010. The proposed method translates tumor DWI signals into cell density and quantifies the whole tumor cell load. The developed method can be applied to other cancer types.

## April 19th, 2016

**
Mario Pereira
** (Toccata (Inria Saclay))

Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.

**
Athmane Bakhta
** (CERMICS)

Many electronic devices such us computers, cellphones, photovoltaic cells, medical devices,...are based on crystals. It is very important to understand the microscopic behavior of such materials. Indeed, the electronic structure of a crystalline material allows for example to determine if it will be insulating or conducting, what is his color, or if it will have some magnetic behavior. But, how to modelize such materials? and how the electronic structure is it calculated? The answer lays in two key-words: Schrödinger equation and Bloch-Floquet transform.

## March 15th, 2016

**
Damien Garreau
** (SIERRA)

(no slides ☹)

The kernel change-point detection algorithm, introduced by S. Arlot, A. Celisse and Z. Harchaoui (http://arxiv.org/abs/1202.3878). The change-points in a piecewise constant signal with values in an arbitrary set are selected via a penalized model selection procedure. In this talk, Damien will show how the correct number and position of the change-points are recovered under suitable hypothesis on the data and the kernel.

**
Renaud Dessalles
** (RAP)

The functional molecules of the cell, the proteins, are produced from the genetic information through an intermediate molecule, the mRNA. This chain of production is highly stochastic (as the result random encounter of macromolecules, thermal excitation etc.) and produces a protein distribution with noticeable variability. In bacteria, for some gene, feedback mechanisms may exist in the protein production. One simplest of them consists in a protein that can bind to the promoter of its own gene, preventing the gene's transcription of mRNA, and therefore the production of the same protein. A stochastic model that represents this particular feedback, called autogenous feedback, is presented. After presenting the model in its biological context, we investigate what features can this autogenous feedback have compared to the models without feedback in terms of distribution and temporal behaviour.

## February 16th, 2016

**
Mikel Landajuela
** (REO)

Mechanical systems involving the interaction of a deformable structure with an internal or surrounding incompressible fluid flow appear in a wide variety of scientific and engineering fields: from the aeroelasticity of sailing boats and parachutes to the biomechanics of blood and air flows. In this talk, I will discuss several novel techniques for the numerical simulation of this type of problems. The basic principle is that, for computational efficiency, the numerical methods must introduce a significant degree of splitting between the fluid and solid time-steppings. Special attention will be paid to problems involving large structural deflections, with solids that might come into contact or that might break up. A series of numerical tests, including comparisons with experimental data, illustrates the performance of the different methods proposed.

**
Jacques-Henri Jourdan
** (GALLIUM)

Maybe you do not know it, but most of you use some sort of compiler (or maybe an interpreter?) in your everyday research activities. But, hold on! What's a compiler? What is it made of? How does it works? What does it means for a compiler to be correct? What are the open questions of this area? In this talk, we will do an overview of all the different components of a compiler, from parsing to assembly code generation, without forgetting to speak about type-checking and code optimization. We will get insight of what it means to prove correct a compiler, such as CompCert, developped in my team, Gallium.

## November 17th, 2015

**
Aiko Dinale
** (RITS)

(no slides ☹)

FURBOT (Freight Urban RoBOTic) is a European project developing an improved system for urban freight delivery. Its centerpiece is a new fully-electrical semi-autonomous vehicle realizing freight transportation. Although travel between the beginning and end points relies on the human driver, the procedures related to loading and unloading are almost entirely automatized. These include the precise docking of the vehicle at the freight boxes prepared for pick-up, as well as at the unloading location. During the presentation, particular attention will be paid to the vehicle control system and the procedures related to the autonomous loading and unloading.

**
Margriet Palm
** (MAMBA)

(no slides ☹)

When a primary tumor spreads to other organs, changes of survival decrease radically because current treatments are rarely able to cure metastatic cancer. If it were possible to block the spreading of primary tumor, metastatic cancer would no longer be a problem. Unfortunately, our current understanding of tumor metastasis is insufficient to block this process. To improve our understanding of tumor metastasis, we built an agent-based model of tumor invasion, which is one of the first steps of metastasis formation. In this model, one or more cells migrate that mechanically and chemically interact with their environment and thereby deforming it such that the cell can migrate.

## October 20th, 2015

**
Chloé Audebert
** (REO)

(no slides ☹)

Liver is an organ which has the ability to regenerate. In order to treat some pathologies, a partial ablation of the liver (partial hepatectomy) is required. Even if the liver regenerates after the surgery, sometimes the new liver is less performant which put in danger patient health. The liver blood perfusion is complex and, after a partial hepatectomy, the remaining portion of the liver experiences important changes in pressure and flow. These changes seem to be the cause for the non-functional liver regeneration. The mathematical modeling could help to better understand and predict the liver hemodynamics after partial hepatectomy. The model needs to be simple enough to be parametrized but complex enough to represent the important effects of the hepatectomy.

**
Aurora Armiento
** (BANG)

(no slides ☹)

Protein aggregation is one of the main causes of neurodegenerative diseases called amyloid diseases (among which are Alzheimer, Huntingtons, Parkinson etc). Moving from Lifshitz-Slyozov equation, we define a model for protein polymerisation. We couple the model to the observation of some moment of the cluster concentration function. The goal is to estimate kinetic coefficients and/or cluster concentration. The estimation is performed by data assimilation methods.

## June 16th, 2015

**
Pauline Traynard
** (LIFEWARE)

Chronobiology, the field that examines biological rhythms, has many promising applications for human health. For example, understanding the links between the cell cycle and the circadian clock in mammalian cells could ultimately help designing cancer chronotherapies. In her talk, Pauline will present systems biology approaches to this problem. In particular she will show how Temporal Logic can be used to calibrate and study the oscillatory dynamics of a bidirectional coupling model of the cell cycle and the circadian clock.

**
Clément Poncelet
** (MUTANT)

The slides — also available in an alternate format

Interactive Music Systems (IMS) are involved in live performances with human musicians and react in realtime to audio signals and unpredictable incoming events. Some of them, as the software Antescofo, are Score-Based IMS: they emit outputs according to a pre-specified timed scenario called a mixed music score. Such systems are used during public concerts and the complexity of the environment (i.e. the human musicians) prevents composers from testing these systems manually. How can we test formally a score-based Interactive Music System? Clément will present us a solution to this problem.

## May 19th, 2015

**
Guillaume Seguin
** (WILLOW)

Digital visual contents are ubiquitous. What can we do with such amounts of visual data? In this talk, we've looked at examples of computer vision applications and approaches on how to model and tackle some of the underlying tasks.

**
Saliha Lallali
** (SMIS)

The slides — also available in an alternate format

Saliha works on a new embedded search engine designed for smart objects. Such devices are generally equipped with extremely low RAM and large Flash storage capacity. To tackle these conflicting hardware constraints, conventional search engines privilege either insertion or query scalability but cannot meet both requirements at the same time. Moreover, very few solutions support document deletions and updates in this context. She introduced three design principles, namely WriteOnce Partitioning, Linear Pipelining and Background Linear Merging, and shown how they can be combined to produce an embedded search engine reconciling high insert/delete/update rate and query scalability.

## April 21st, 2015

**
Guillaume Claret
** (PI.R2)

We presented the Coq system by a demo session. Coq is a software used to check mathematical proofs or to write safe programs. More and more people see the formal verification as a required step to make sure that (complex) proofs are correct. The powerful Coq axioms (different than the sets theory) can also open alternative and elegant ways to formalize problems.

**
Rémi Lajugie
** (SIERRA)

Learning tasks involving structured outputs such as graphs, sequences are ubiquitous. Dealing with them require specific algorithms. In this talk, we focused on cases where the learning task involve a temporal structure (such as time warping or change-point detection). We presented some applications to music information retrieval and computer vision.

## March 17th, 2015

**
Joachim Cohen
** (QUANTIC)

The slides — also available in an alternate format

A quantum computer could solve problems inaccessible to classical ones. However, such a machine would suffer from the fragility of the quantum systems due to their interaction with the environment. A solution to this major issue is provided by quantum error correcting codes, but their efficient implementation remains an important experimental challenge. Joachim told us how a carefully engineered interaction of the system with its environment circumvents the need for feedback control, thus realizing autonomous quantum error correction.

**
Luca Nenna
** (MOKAPLAN)

Luca gave a general overview of the optimal transport problem and its extension to the multi-marginal framework (numerical simulations helped us to understand this nice theory!). Then he introduced an application of optimal transportation to quantum mechanics in order to understand the electronic configuration of atoms and molecules.

## February 17th, 2015

**
Pierre-Marie Pédrot
** (Pi.r2)

Pierre-Marie Pédrot spoke about the Curry Howard correspondence : this concept, used by computer science logicians, introduce a deep link between the notions of program and the notion of proofs. He will explain why, when you are proving a theorem, you are likely to be also writing a program, and, conversely, when you are writing a program, you are not far from proving a theorem. This idea is at the very core of the Coq proof assistant, which let you both write program and prove theorems at the same time.

**
Arnaud Lionnet
** (MATHRISK)

Arnaud has presented the basic problem of pricing and hedging derivative contracts in finance. Derivatives are contracts that pay an amount of money dependent of what another financial asset does. This problem is really at the heart of what quantitative analysts do in banks. for this, he has introduced backward stochastic differential equations, which provide a natural language to cast the pricing and hedging problem.

## Juanuary 20th, 2015

**
Jean Thorey
** (CLIME)

(no slides ☹)

Jean will explain how to forecast global solar radiation from numerical weather predictions.

**
Zuqi Tang
** (POMDAPI)

Zuqi told us about different kinds of errors in mesh-based numerical methods, and explaind us how to tweak algorithm in order to balance them.

## December 16th, 2014

**
Géraldine Cellière
** (MAMBA)

The slides — also available in an alternate format

The body is a tightly regulated machinery and a lot of compounds are maintained within narrow concentration ranges for a good functioning. One of the main regulating organs is the liver. But with medicines and alcohol intake, you make life tough for your liver! What happens when the liver is damaged for example in the case of a paracetamol overdose or cirrhosis? Because measuring processes in vivo is challenging, we use multi-scale mathematical modeling strategies to investigate the liver’s adaptation to acute injury focusing on ammonia detoxification. Based on existing data and literature knowledge, these models examine the plausibility of different hypotheses to guide towards new informative experiments.

**
Lucile Megret
** (MYCENAE)

Many natural phenomena can be described by slow-fast systems, where a fast transition between a state of equilibrium and relaxation oscillation is modelised with a canard explosion. Lucile told about a category of Liénard's slow-fast systems and present a first approach to investigate the possibility of bifurcations displaying a dramatic change in the phase portrait in a very small change of a parameter. After a presentation of some theoretical and numerical tool, she provided an example of such a very rapid loss of stability on a specific example using classical numerical continuation.

## November 18th, 2014

**
Victorien Menier
** (GAMMA3)

Victorien told us about Mesh Adaptation, Fluid Dynamics and Aeronautics. He explained us what are adapted meshes, and why they are very useful to accuratly and efficiently simulate non-viscous flows using Euler equations. Then, he explained what difficulties he faces to extend these techniques to Navier-Stokes equations, that take into account viscosity.

**
Nicholas Tarabelloni
** (REO)

Nicholas told about how to make a computer able to analyze an electrocardiogram. His aims are both to be able to computationally distinguish pathological and physiological states, but also to assess the validity of synthetic signals.

## October 21st, 2014

**
Emilie Kaufmann
** (DYOGENE)

Emilie spoke about sequential resource allocation. This mathematical concept is widely used, from recommender systems and on-line advertisement to clinical trials. In this framework, an agent is facing an unknown environment, consisting of several options with random outcomes. Emilie presented strategies such an agent can have to decide which option he wants to try, in an adaptive way (i.e. based on the results of previous trials). His strategy should achieve a trade-off between exploration (trying options with a lot of uncertainty) and exploitation (focusing on options he thinks are best). In her talk Emilie presented a statistical model called the 'stochastic multi-armed bandit' (in reference to the optimal choice of a slot machine -also called "one-armed bandit"- in a casino). She introduced a notion of optimality and presented strategies based on several statistical tools.

**
Guillaume Trehard
** (RITS)

Guillaume told us about "Ego-localization" for autonomous vehicles. As some of you have seen in the "salon de l'auto" in Paris, autonomous riving is a fast growing problematic. Yet, it is still a real challenge. Guillaume presented solutions of a particularly crucial challenge: the precise localization of the vehicle, in its environment and in a global map. Taking the most of information fusion and data filtering methods, his solutions provide under meter precision while being reasonably expensive in terms of money, data and developing time.

## June 17th, 2014

**
Elisa Schenone
** (REO)

Elisa simulates the electrical behavior of the heart with complex equations. Since classical numerical techniques such as the Finite Element Method (FEM) can require a long time to be solved, she presented two techniques of Reduced-Order Method (ROM) used to decrease the dimension of the basis, i.e. the space where equations are solved: the Proper Orthogonal Decomposition (POD) and a new method based on Approximated Lax Pairs (ALP).

**
Chantal Keller
** (PROSECCO)

Chantal presented F*, a programming language by Inria and Microsoft with precise types designed for program verification. She explained the main ideas behind the design of such a language, and the current questions that arise, e.g. to deal with higher-order programs, side effects, non-termination...

## May 20th, 2014

**
Pierre Merdrignac
** (RITS)

Pierre presented his research in the team RITS, a multidisciplinary project carrying out R&D activities for Intelligent Transportation Systems (ITS). This domain aims at improving road transportation in terms of safety, efficiency, comfort and also to minimize nuisances. RITS develop multidisciplinary ideas from robotics, communications, and traffic modeling. In his talk, he introduced the applicability and performances of laser-based pedestrian detection and vehicle to pedestrian communication for safety of vulnerable road users.

**
Cuong To
** (SMIS)

Cuong works on the critical issue of personal data which usually ends-up on central servers. Cuong showed us how decentralized data storage architectures can help individuals keep full control of their data. He presented secure distributed querying protocols and showed how to secure their execution in the presence of honest-but-curious attackers, without revealing any sensitive information to central servers.

## April 15th, 2014

**
Pietro Gori
** (ARAMIS)

Pietro talked about statistical methods for the analysis of neuronal connectivity in patients with Gilles de la Tourette syndrome (GTS). He analyses structural and diffusion images of the brain with a novel atlas construction procedure to capture the invariants of both GTS patients and control subjects, and identify atypical anatomical configurations of neural circuits in patients.

**
Wafaâ Haffaf
** (MAMBA)

Protein aggregation leading to the formation of amyloid fibrils is involved in several neurodegenerative diseases such as prion diseases. Wafaa presented two models to clarify how these fibrils are able to incorporate additional units. The initial model, adapted from the Becker-Döring system that considers that all fibrils react similarly but is not able to reproduce the observed in vitro behaviour. It comes then a second model which involves an additional compartment of fibrils unable to incorporate more prion units and correctly simulates the first experimental steps for prion aggregation.

## March 18th, 2014

**
Caterina Urban
** (ANTIQUE)

Caterina introduced us to abstract interpretation, a framework able to automatically prove some properties on programs. In particular, she presented abstract domains for proving termination of programs. The domains automatically synthesize piecewise-defined ranking functions and infer sufficient conditions for program termination. With her team Caterina has implemented a prototype static analyzer for proving termination of programs which is competitive with the state of the art and performs well on a wide variety of benchmarks.

**
Soledad Fernandez Garcia
** (MYCENAE)

Soledad presented her PhD work on Melnikov theory for planar hybrid systems. At the present time, the study of piecewise-smooth dynamical systems is enjoying a great popularity due to its capability to model mechanical devices, electronic circuits, control systems and biological problems, inter alia. In hybrid systems, each zone of differentiability is separated by a straight line. When an orbit reaches the separation line, then a reset map applies before entering the orbit in the other zone. Soledad showed us how to use Melnikov functions to analyze the existence of limit cycles. The results have been applied to the study of invariant cones in 3D piecewise linear systems.

## February 13th, 2014

**
Fajwel Fogel
** (SIERRA)

Fajwel works on convex relaxations of non-convex problems. Convex optimisation deals with finding the minimum of convex functions, for instance to fit the parameters of a model etc. Although many real-world problems are not convex, it is sometimes possible to write a convex relaxation of the original problem and thus compute an approximate solution to it. Fajwel gave examples of this technique in X-ray molecular imaging, and DNA sequencing.

**
Roxana Dumitrescu
** (MATHRISK)

(no slides ☹)

Roxana presented the reflected backward stochastic differential equations (RBSDEs), driven by the brownian motion and the Poisson random measure. RBSDEs represent a very useful mathematical tool in financial mathematics. Roxana gave some applications in the case of risk measures and pricing of American Options.

## January 21st, 2014

**
Stephanie Lindsey
** (REO)

(no slides ☹)

Stephanie presented her experimental work that involves altering flow patterns early on in development and studying their effects on subsequent cardiac formation. She then explained the benefits of coupling these experiments with computational fluid dynamics. Her work aims to determine the cause of some of the more severe congenital heart defects that present themselves clinically.

**
Henning Sulzbach
** (RAP)

The probabilistic analysis of algorithms is a research area on the edge between mathematics and computer science. One of its founders, Philippe Flajolet, spent his academic career at Rocquencourt. Henning started with a short introduction to the field. Then, he presented one of the main results of his thesis (Frankfurt, 2012) concerning the complexity of certain search operations in multidimensional data structures. He provided insight to the underlying mathematical ideas without giving technical details.

## December 17th, 2013

**
Adrien Guatto
** (PARKAS)

The slides — also available in an alternate format

Adrien works on synchronous programming and told us about stream equations and nested loops. Equations over finite data streams are a classic formalism used during the design phase of embedded systems. Compilers for specialized streaming languages are able to translate such equations to low-level source code written in C, and have met a resounding success in industrial practice. He presented his ongoing work aimed at generating better code from these streaming languages.

**
Valentin Suder
** (SECRET)

Valentin works on symmetric cryptography and boolean functions. Because of their link with digital logic, boolean functions are fundamental in computer science. In this talk Valentin focused on cryptographic applications. We saw how Boolean functions can help to model cryptographic objects, to emphasize security criterions and to analyze block ciphers. We also saw why designing boolean functions that have the best resistance against some attacks is a difficult task.

## November 19th, 2013

**
Simon Marmorat
** (POEMS)

Simon showed us how wave propagation can be disturbed by small heterogeneities in the media. He explained why simulating the propagation of waves inside such medium is challenging for classical numerical tools and how its complexity and computational costs can be reduced by introducing an 'easier' approximate model.

**
Andres Gonzalez
** (CONTRAINTES)

Andres talked about experimental techniques in biology that allow tracking of gene expression in single cells over time. So far, few attempts have been made to fully exploit this data for the modeling of biological networks and cell population dynamics. Andres uses it to develop models that are able to predict gene expression at the single-cell and population level.

## October 22nd, 2013

**
Jessica Oakes
** (REO)

(no slides ☹)

Jessica talked about aerosolized therapeutics and treatments of lung diseases, e.g. lung cancer or asthma. She presented her experimental and numerical studies on rat emphysema, a chronic obstructive pulmonary disease caused by inhaling toxic particles and gases over a long period of time.

**
Rémi Varloot
** (DYOGENE)

Rémi began with a presentation of Markov chains and of their applications. He then gave details concerning the study of their evolution, and commented on the difficulty of creating random samples of the system in its equilibrium. He presented two algorithms that achieve this, "Monte Carlo Markov chains" and "coupling from the past", and concluded by introducing a variant of the latter.

## September 17th, 2013

**
Antoine Delignat-Lavaud
** (PROSECCO)

Antoine explained how he works to prevent various kinds of web attacks and trojan programs. He presented tools and models he developed to verify web applications and explained their implementation against a realistic web attacker.

**
Ali Assaf
** (DEDUCTEAM)

Ali presented proof systems tools which help to write better software. Many proof systems exist; Ali showed how translating them to a single unified proof framework can improve their interoperability.

## June 18th, 2013

**
Jonathan Protzenko
** (GALLIUM)

Jonathan gave us a controversial talk about why we need type-checking in programming languages. Drawing inspiration from an actual story, he told us the story of a person who wants to start programming but encounters a compiler error. Moving on, he introduced the audience to the life of a researcher in the field of programming languages, the theorems that they have to prove to earn a living, and the kind of results that they want to achieve.

**
Emanuele Leoncini
** (RAP)

The slides — also available in an alternate format

Emanuele told us about his exciting research work. Emanuele, when he's not busy running or swimming, works on modeling protein production inside cells. This requires the use of ∭ integrals, Poisson point processes, and advanced mathematics and biology. In his talk we learned all about bacteria and how they're being studied!

## May 21st, 2013

**
Mathieu Leconte
** (DYOGEN)

Mathieu presented two applications of generalized matching in random graphs. The first application deals with the optimization of storage in a distributed manner, in order to optimize content delivery networks, such as YouTube and more generally video-on-demand systems. The second application analyses the performance of multiple-choice hashing techniques.

**
Faten Nabli
** (CONTRAINTES)

Faten explored the structural properties of Petri nets as a means to provide information about the evolution of a biochemical system and its dynamics, especially when kinetic data are missing, thus making simulations impossible. In particular, the structural properties of siphons and traps will be enumerated using a boolean model, while place and transition invariants will be analyzed using constraint programming.

## April 23rd, 2013

**
Senanayak Karri
** (SIERRA)

Submodular functions are a useful class of discrete set functions in various areas such as economics, computer vision, machine learning, computer networks, operations research etc. Optimization of submodular functions is a problem that lies on the boundary of efficiently computable(P) and not efficiently computable(NP) class of problems. Sesh gave an overview of different algorithms proposed to perform optimization efficiently.

**
Joshué Perez
** (IMARA)

(no slides ☹)

In the last years, mass-produced vehicle implementations have been done in the field of intelligent Transportation System (ITS). The Advanced Driver Assistance Systems (ADAS), intelligent infrastructures and autonomous driving maneuvers have significantly contributed to the implementation of intelligent systems on the road and in urban areas. Thanks to research done by many groups and projects is possible to find safer and more comfortable vehicles. Some examples are: Antilock Brake System (ABS), Cruise control (CC), Automatic parking and Electronic Stability Control (ESC), among others. At this time, it is not a utopia to think that, in a close future, autonomous vehicle will coexist with other conventional vehicles, interacting with them. In this work, different control systems for autonomous vehicles have been developed, both individual and cooperative maneuvers in different urban and highway scenarios. Using previous works in the lateral and longitudinal controller, different experiments have validated the modular control architecture, independent of the vehicle and the scenario used, described in this paper. To realize these experiments, different platforms have been used. Electric and gasoline-propelled vehicles for urban environment, that is: straight and curve segments, blocked roads, overtakings, commucations between infrastructure and vehicles and high speed experiments have been used. Furthermore, this control system is easy to tune, based on fuzzy logic techniques and human knowledge, and it has been extended to different maneuvers.

## March 26th, 2013

**
François Durand
** (GANG)

François gave an introduction to voting systems. Voting systems are useful not only for elections, but also in computer systems such as routing, where entities have to make choices for the best route possible. After trying to understand what is a "good" voting system, and whether such a good voting system exists, we saw how we can try to manipulate the results of an election, and what we can do about it.

**
David Benoît
** (MICMAC)

David told us about the mathematical analysis of models for a non-Newtonian fluid. Numerous problems, especially in civil and environmental engineering (rivers, avalanches, mudslides) require simulations of non-Newtonian fluids. Compared to Newtonian fluids, which can be modeled with the Navier-Stokes equations, the non-Newtonian nature brings new nonlinearities that complicate the modeling and numerical simulation of such fluids.

## February 26th, 2013

**
Cédric Pasteur
** (PARKAS)

Cédric gave us an introduction to time and concurrency in programming languages, more specifically, synchronous functional programming languages, such as ReactiveML. The talk featured several amazing demos, including one with a famous plumber from a well-known video game.

**
Nick Jagiella
** (BANG)

(no slides ☹)

Nick, after successfully defending his PhD, summed it up for us: we learned how cancer works, in particular, what kind of mechanisms come into play when modeling cancerous cell growth. Nick connected together both a macroscopic point of view and a microscopic perspective, and showed how successful modeling can help give better predictions for patients.

## January 15th, 2013

**
Gregory Arbia
** (REO)

Congenital heart defects are the leading cause of birth defects, affecting 1% of in live births. For many of them, several surgeries are needed. Modeling of blood flow becomes a tool for understanding a disease, or to simulate different surgical options. The magnetic resonance imaging can construct a three-dimensional geometry and flow measurements. On the other hand, using a catheter, blood pressure measurements are done. Then it is to simulate the flow of blood in the discretized field and to model the effect of the structure downstream. At this end a coupling between the partial differential equations of Navier-Stokes equations and ordinary differential equation is performed at each output of three-dimensional domain. Issues of this study are numerical and clinical. On the one hand it is necessary to deal with problems related to coupling instabilities, and on the other hand clinicians want a reliable representation of the flow of blood in the area of interest. The results are presented for five patients who underwent a so called Norwood procedure, connecting the systemic network to the arterial network close to the heart.

**
Jaime Gaspar
** (PI.R2)

Proof interpretations are tools in mathematical logic with many applications: for example, consistency results, unprovability results, and extraction of computational content from proofs, to name a few. In this talk we are going to introduce proof interpretations and to present examples of their applications. We keep the talk short, simple and sweet.

## December 14th, 2012

**
Francesco Santini
** (CONTRAINTES)

Semiring-based Soft Constraints provide a mean to associate a score to the satisfaction of classical crisp constraints. In this way, it becomes possible to represent users' preferences, to solve over-constrained problems, and to optimize weighted problems in general. In this talk, Francesco introduced the general formal framework, and an application to Abstract Argumentation Frameworks.

**
Benjamin Aymard
** (SISYPHE)

An ovarian follicle is a spherical shelter for oocyte, in the ovaries. The selection process ends by ovulation, in the best case, bust most of the time by atresia (degeneration). We study the problem of the selection process of the ovarian follicles. At micro scale, the model is a 2D hyperbolic system of conservation laws of size 20 times 20 with discontinuous fluxes on interfaces. At macro scale, we have a closed loop control. The coupling between micro and macro is done by the moments of the solution. In order to obtain numerical simulations of such a model we use parallelization and high order finite volume schemes. The strategy in the computations is to use an analogy with the biology.

## November 20th, 2012

**
Thibaut Balabonski
** (GALLIUM)

Thibaut explained to us how to save time in a computation by cheating the system in order to build simple optimal evaluation strategies in any programming language.

**
Saverio Smaldone
** (REO)

Saverio told us how to split the complexity the cardiovascular system by coupling the blood flow in the different cardiovascular compartments.

## October 16th, 2012

**
Steven Gay
** (CONTRAINTES)

Steven told us how he uses contraints programming to efficiently solve problems on graphs that model biological reactions.

**
Anne-Céline Boulanger
** (BANG)

Anne-Céline explained to us how to optimize microalgae growth, a complex problem with many parameters -- algae could serve as a potential source of biofuel in the future.

## September 18th, 2012

**
Gabriel Scherer
** (GALLIUM)

Gabriel gave a very engaged talk about how real-world languages are poorly designed, and how the programming language community can help prevent design mistakes. This talk bashed various languages such as Python, Javascript, PHP...

**
Cécile Mailler
** (LMV)

Cécile introduced us to the topic she worked on during her master's internship, namely, random boolean binary trees. She gave a very accessible introduction to the main result about these trees, and gave proof sketches using two different techniques.

## June 26th, 2012

**
Filippo Visco Comandini
** (SISYPHE)

Filippo gave us an introduction to electrical networks, and how to detect faults in them. Like many other research topics, this is motivated by industrial concerns, especially in airplanes, where diagnosing faulty components in crucial.

**
Aliénor Burel
** (POEMS)

The slides — also available in an alternate format

Aliénor told us about wave propagation in soft materials. Modeling such phenomena involves complex mathematical equations, and a lot of numerical analysis.

## May 15th, 2012

**
Mathieu Feuillet
** (RAP)

Mathieu works on network modeling. He uses probabilities and queuing networks; there are various applications, and the one he chose to present is the study of congestion in the Internet network. His worrying talk was entitled « Is the Internet doomed to collapse? ».

**
Estelle Mbinky
** (GAMMA)

Estelle works on mesh generation algorithms. Problems include mesh refinement, and applications include various modeling situations, such as planes. She told us about error control for anisotropic physics problems.

## April 10th, 2012

**
Jérémie Lumbroso
** (ALGORITHMS)

Jérémie gave us an introduction to probabilistic algorithms. In particular, he showed us how probabilistic counting algorithms allow one to watch a flow of data, and count items in real-time, while using less bits than required and still giving an accurate estimate. Applications include sequence counting in DNA, filtering out duplicates in search results...

**
Alexandre Imperiale
** (MACS)

Alexandre works on heart modeling. He told us about his favorite pig, and how he modeled his heart, then made a barbecue out of it. There are various problems involved with heart modeling: one of them is data assimilation, that is, finding parameters so that the simulation matches observations as close as possible.

## March 20th, 2012

**
Luna Dimitrio
** (BANG)

Luna works on p53, a super-powerful protein. When the cell is shocked, p53 is able to suspend the cellular division while the cell heals; if the cell is damaged beyond repair, p53 will kill the cell. Luna explained the different feedback mechanisms, and how, introducing a spatial aspect in her differential equations, she was able to accurately modify the oscillations in the concentration of p53.

**
Pawan Goyal
** (SANSKRIT)

Pawan works on text analysis: he told us how, using various techniques, he was able to improve the quality of information retrieval in various documents, and improve text summarization as well. He described the various challenges in extracting relevant extracts from documents.

## February 14th, 2012

**
Amel Bennaceur
** (ARLES)

Amel's work is about making different, apparently incompatible systems talk together. This is particularly useful in emergency response situations, where you have to make different entities work together. By reasoning formally on what different systems expect, she is able to dynamically generate glue that ties these different systems together.

**
Jannis Uhlendorf
** (CONTRAINTES)

Jannis' work is about proteins, and how to engineer them so that they behave differently. By using a control-command system, he is able to control the development of these proteins.

## January 17th, 2012

**
Karim Drifi
** (CLIME)

Karim works in climate modeling; he tries to predict the velocity of fluids, such as the sea, using imagery data, e.g. temperature measurements obtained from a satellite. These models require tremendous computing power, and his job is to invent new techniques so that the modeling becomes tractable.

**
Yanli Guo
** (SMIS)

Yanli works with embedded databases in smart cards. The very specific constraints of such chips require sophisticated algorithms to provide cryptographic guarantees while still coping with the limited capabilities of the chips, and this is what Yanli's works are about.

## December 20th, 2011

**
Émilie Coupechoux
** (TREC)

Émilie told us how she uses graphs to model epidemics propagation; how the presence of clusters, or communities, in graphs, allows one to better understand how epidemics propagate; and how this relates to real-life situations.

**
Cristóbal Bertoglio
** (REO)

Cristóbal introduced us to fluid-structure interactions, and how we can use them to measure artery stifness: this has many application, especially in diagnosing and measuring congenital heart diseases.

## November 15th, 2011

**
Christina Boura
** (SECRET)

Christina introduced the audience to cryptographic hash functions, their properties, and what makes a hash function a good one.

**
William Weens
** (BANG)

The slides — also available in an alternate format

Wiliam Weens talked about liver cancer, and how to use an agent-based model to reason about cell interactions, which may lead to a better understand of the various cancer types.

## October 18th, 2011

**
Thierry Martinez
** (CONTRAINTES)

Thierry Martinez discussed constraint logic programming, and illustrated his talk with the Sudoku game as an example.

**
Daniele Trimarchi
** (MACS)

(no slides ☹)

Daniele Trimarchi gave a talk about to model difficult physical phenoma such as wind in yacht sails, using advanced modelisation techniques.

## September 20th, 2011

**
Marc Mezzarobba
** (ALGORITHMS)

Marc gave a talk on computer-assisted symbolic computations on mathematical functions.

**
Alexandre Pilkiewicz
** (GALLIUM)

Alexandre gave a talk about formally verifying the compilation process using the CompCert verified compiler, and why certified compilation is important in life.