Current research at the Joint Centre is presented at Forum 2011
The Microsoft Research-INRIA Joint Centre has been created in October 2005. Three research projects started in May 2006, followed by six more since 2007.
The research programme is divided into three tracks.
A) Software Security and Trustworthy Computing, comprising 3 projects: Mathematical Components, Tools and Methodologies for Formal Speciﬁcations and for Proofs, and Secure Distributed Computations and their Proofs.
B) Computational Sciences and Scientiﬁc Information Interaction, comprising 4 projects: Dynamic Dictionary of Mathematical Functions, ReActivity, Adaptive Combinatorial Search for E-Science, and Image and Video Mining for Science and Humanities.
C) Applications of Cloud Computing, comprising 1 project: Neuroimaging and Azure platform.
Come and meet the MSR-INRIA researchers !
Our Forum 2011 is followed by the Software Summit 2011.
09:30 Welcome Address Andrew Blake, Managing Director, Microsoft Research Cambridge Michel Cosnard, CEO, INRIA
09:45 Mathematical Components (slides) Assia Mahboubi, INRIA
10:10 Secure Distributed Computations and their Proofs (slides) Cédric Fournet, Microsoft Research Cambridge
11:00 TLA+ (slides) Damien Doligez, INRIA
11:25 Dynamic Dictionary of Mathematical Functions (slides) Frédéric Chyzak, INRIA
11:50 A-Brain (slides) Gabriel Antoniu, INRIA Bertrand Thirion, INRIA
12:15 Lunch and Demos
14:00 ReActivity Jean-Daniel Fekete,INRIA,
14:25 Adaptive Combinatorial Search for e-Sciences (slides) Youssef Hamadi, Microsoft Research Cambridge Marc Schoenauer, INRIA
14:50 Scientific Image and Video Data Mining (slides) Jean Ponce, Ecole Normale Supérieure
15:15 Break and Demos
16:00 Panel on Formal Methods Christine Paulin (Paris-Sud), Cédric Fournet (Microsoft Research Cambridge), Tony Hoare (Microsoft Research Cambridge), Peter Paule (J.Kepler University, Linz), David Pointcheval (Ecole Normale Supérieure), Mark Ryan (University of Birmingham), Wolfram Schulte (Microsoft Research Redmond); Jean-Jacques Lévy (INRIA, Director of the Microsoft Research-INRIA Joint Centre).
17:00 Demos and Cocktails
You are kindly invited to participate to Forum 2011 and discover recent research at the MSR-Inria Joint Centre. There will be eight scientific talks and demos.
Attendance, food and cocktail are free.
Registration was before April 5, 2011, but is still feasible by clicking below.
More Information and registration:
Phone : +33 1 69 35 69 70
The Campus Microsoft is located close to Boulevard Périphérique and la Seine river. It is accessible by Métro, RER, Tramway or Bus. See following maps.
Formalized mathematical theories can, like modern software, be built out of components. By components we mean modules that comprise both the static (objects and facts) and dynamic (proof and computation methods) contents of theories. We develop a general platform for mathematical components, based on the Coq "ssreflect" extension that was used to carry out the formalization of the Four Colour Theorem. We would validate the platform on a significant development: the historical proof of the Odd Order theorem.
We present programming tools for building distributed applications with strong security guarantees. Given some security goals and attacker model, our tools produce executable code and their security proof. In particular, they generate and verify cryptographic protocols to protect the application, even when large parts of the computation are controlled by the attacker. We illustrate our approach on multiparty sessions, information-flow security, and the TLS protocol.
TLA+ is a specification language especially suited to describing and formally specifying concurrent and distributed systems. TLA+2 is the next version of TLA+, which adds a proof language that allows writing formal proofs of correctness of systems specified in TLA+. In addition to TLA+2, we will present the tools we are developing to help engineers write and certify proofs in TLA+2.
The project aims at providing a web encyclopedia of mathematical functions that is completely computer generated. The framework is given by computer algebra algorithms for solutions of linear differential equations. While developing new algorithms in this area, we also started to work on defining a language for developing dynamic mathematics on the web. In this talk, we give an overview of our aims, our methods and a short demo of our prototype.
Joint acquisition of neuroimaging and genetic data on large cohorts of subjects is a new approach used to assess and understand the variability that exists between individuals, and that has remained poorly understood so far. As both neuroimaging- and genetic-domain observations represent a huge amount of variables, performing statistically rigorous analyses on such amounts of data represents a computational challenge that cannot be addressed with conventional computational techniques. The project investigates the benefits of integrating BlobSeer, a scalable cloud data management system, developed by the Kerdata INRIA team, with Microsoft Azure storage services and aims at evaluating the impact of using BlobSeer on Azure with large-scale application experiments such as the genetics-neuroimaging data comparisons addressed by the Parietal INRIA team.
12:15 Lunch and Demos
The goal is to explore how to capture and visualize user activity, to enable scientists and groups of scientists to reflect upon, and to interact with and improve their research processes. We intend to develop sophisticated strategies for logging activity with bilateral links between on-line and off-line data, and powerful methods for visualising across multiple scales and interacting with the results.
Adaptive Search is concerned with automatic tuning of parameters in search algorithms. Three different types of algorithms have been already addressed by our project: an innovative Constraint Programming heuristic which adapts to the observed performance of past decisions; an Adaptive Operator Selection in Evolutionary Algorithms with Multi-Armed Bandit techniques; and a variation on the Covariance Matrix Adaptation Evolution Strategy (either specializing or generalizing its adaptive scheme) in the context of continuous optimization.
Our research is about mining dynamical remote data with applications in computational ecology and environmental science, mining historical collections of photographs and paintings with applications to archaeology and cultural heritage preservation, and mining TV broadcasts with applications to sociology.
15:15 Break and Demos
16:00 Panel on Formal Methods
Chirstine Paulin (Paris-Sud), Cédric Fournet (Microsoft Research Cambridge), Tony Hoare (Microsoft Research Cambridge), Peter Paule (J.Kepler University, Linz), David Pointcheval (Ecole
Normale Supérieure), Mark Ryan (University of Birmingham), WolframSchulte (Microsoft Research Redmond); Jean-Jacques Lévy (INRIA Director of the Microsoft Research-INRIA Joint Centre).
17:00 Demos and Cocktails