In May 2006, on the Plateau de Saclay, about 20 kilometers south of Paris, three research projects in the fields of formal methods and security were launched at the brand-new, Orsay-based Microsoft Research-INRIA Joint Centre.
The lab, founded by the Institut National de Recherche en Informatique et en Automatique (INRIA)—the French National Research Institute for Computer Science and Applied Mathematics—along with Microsoft and Microsoft Research Cambridge and officially inaugurated on Jan. 12, 2007, established as its objective the pursuit of fundamental, long-term research in formal methods, software security, and the applications of computer-science research to the sciences.
On Jan. 28, in Palaiseau, France, at the Amphithéâtre Pierre Faurre on the campus of École Polytechnique, more than 200 French academics gathered for the Microsoft Research-INRIA Joint Centre Forum 2009, focused on recent research at the Joint Centre. Attendees heard about the progress achieved since the inception of the lab.
How best to measure that progress? One method to attempt an assessment could be to examine the contributions to the greater research community:
- 118 papers published in academic journals, presented during prestigious conferences and workshops, or published as technical reports.
- Participation in dozens of events, conferences, workshops, seminars, presentations, and invited talks.
Alternatively, you could consider the innovative software and tools designed and implemented, in research areas as diverse as mathematics, image and video mining, and secure distributed computing―all available for download by the research community.
Then there is the research personnel involved:
- INRIA has contributed 31 researchers, a system engineer, and two lab directors, including Jean-Jacques Lévy, INRIA research director, who heads the Joint Centre.
- Microsoft Research has contributed 14 researchers, and the lab’s deputy director, Pierre-Louis Xech, is from Microsoft France.
- Five researchers from other French academic institutions are working on Joint Centre projects.
- 19 Ph.D. candidates have participated in Joint Centre research. Three of them have defended their theses already.
- 16 post-doctoral researchers have been hosted by the Joint Centre.
- The Joint Centre, which currently includes 15 resident researchers, 14 Ph.D. students, and 9 post-docs, has funded 28 person-years of Ph.D. students and 26 person-years of post-docs. This support is helping to grow the talent pool available to the French research community.
No matter how you look at it, the Microsoft Research-INRIA Joint Centre―an extension of an informal but long-term relationship between two giants of European computer science, the late Roger Needham, founding director of Microsoft Research Cambridge, and the late Gilles Kahn, then INRIA chairman―has proven a resounding success.
Andrew Herbert, managing director of Microsoft Research Cambridge
“Both Microsoft Research and INRIA have world-leading computer-science research laboratories,” notes Andrew Herbert, Microsoft distinguished engineer and managing director of Microsoft Research Cambridge. “By combining our strengths, we have been able to tackle some of the most significant challenges in computer science.
“In just two years, the joint laboratory has created incredible momentum: an outstanding number of publications in major international journals and conferences; software prototypes made available to the wider research community; hosting workshops and events attracting participation from Microsoft, INRIA, and French academics; and advanced training for post-docs and Ph.D. students. Many of the results arising from the joint work have contributed progress in Microsoft’s own research and, through that, a direct impact on Microsoft product development and strategies. Working together, we have accomplished more than either partner could have done alone.”
Michel Cosnard, INRIA chairman and chief executive officer, concurs―and regards the Joint Centre as the natural extension of a proud tradition.
“European research and education have always been excellent in theoretical computer science and mathematics, in particular in France,” Cosnard says. “By grounding our collaboration in our strengths and expertise and by exploring promising challenges, Microsoft researchers and INRIA researchers open new avenues in computer programming and software production―and provide new tools for scientists in other disciplines to progress.
“The results are already impressive. But what is most impressive is the quality of the relationships between Microsoft Research and INRIA researchers: full respect, trust, and confidence.”
The path to the creation of the Joint Centre began in April 2005, with the signing of a memorandum of understanding by François d’Aubert, French secretary for Research; Kahn; and Steve Ballmer, Microsoft chief executive officer. In October of that year, François Goulard, French minister of Higher Education and Research, joined Kahn and Microsoft Chairman Bill Gates in signing a framework agreement. The new lab was established near the campus of INRIA Saclay.
Under the direction of leading INRIA researcher Lévy and with strong political support from the French government, the Joint Centre operates on a model of equally shared investment. INRIA provides space and infrastructure. Microsoft France helps with administration and public relations. Researchers from both Microsoft Research and INRIA make visits ranging from a week to years. INRIA hires post-docs and Ph.D. to staff projects led collaboratively by researchers from both Microsoft Research and INRIA.
In addition, all intellectual property created by the Joint Centre is jointly owned. Both INRIA and Microsoft Research have equal exploitation rights to the intellectual property created. And, as noted, the lab is strongly committed to open publication and community software.
Nearing its third anniversary, the Joint Centre currently boasts a two-track research program comprising seven distinct projects, most of them collaborations between INRIA and Microsoft Research. Track A, Software Security and Trustworthy Computing, focuses on the application of mathematics to increasing the security and reliability of software and computing systems through formal specification, tools for verification, and theorem proving or computer-assisted proofs. Track A consists of three projects:
- Mathematical Components.
- Tools and Methodologies for Formal Specifications and for Proofs.
- Secure Distributed Computations and Their Proofs.
Track B, Computational Sciences and Scientific Information Interaction, addresses efficient management and analysis of, and interaction with, increasingly highly complex scientific data. This work is part of growing Microsoft commitment to use of computing concepts and techniques by mathematics, engineering, life-sciences, and physical-sciences researchers. It includes four projects, most of them quite young:
- Dynamic Dictionary of Mathematical Functions.
- Adaptive Combinatorial Search for E-Science.
- Image and Video Mining for Science and Humanities.
“Microsoft researchers and INRIA researchers are supported by talented young post-docs and Ph.D. students advancing the state of the art in two areas: trustworthy computing and scientific-information manipulation,” Herbert explains. “The first theme is about techniques to produce software that is more secure and reliable, a necessary condition as computers become more and more embedded in everyday life. The second theme is about helping scientists in other fields to use computers to accelerate the pace of discovery in areas such as healthcare and well-being, and managing and making more efficient use of the natural environment.”
The seven projects currently being researched at the Microsoft Research-INRIA Joint Centre:
TRACK A: SOFTWARE SECURITY AND TRUSTWORTHY COMPUTING
- Started: Summer 2006.
- Team leader: Georges Gonthier, senior researcher at Microsoft Research Cambridge.
- Project summary: Computer-assisted reasoning has been driven mostly by applications in computer science, but paradoxically, it has yet to gain widespread acceptance in its original domain of application, mathematics. The Mathematical Components project is designed to demonstrate that formalized mathematical theories can be built out of components, modules than comprise both static (objects and facts) and dynamic (proof and computation methods) contents of theories.
- Progress achieved: The team, jointly based in Orsay and Sophia Antipolis, has released ssreflect, a new proof language for the Coq proof system that makes it easier to integrate relevant technical details into a high-level proof text without disrupting or overly expanding it.
- Comment: “Attempts to formalize large proofs have long stumbled on the difficulty of formalizing basic mathematical knowledge, such as the manipulation of sums, in a usable form,” Gonthier says. “Combining type and proof theory with modern software-engineering techniques, we have created a set of mathematical components that capture both mathematical theories and the pragmatics needed to use them effectively. We have used these components to make significant progress in the formalization of the Feit-Thompson Odd Order Theorem, which is the first major step of one of the greatest achievements in contemporary mathematics: the complete classification of finite simple groups.”
Tools and Methodologies for Formal Specifications and for Proofs
- Started: Summer 2006.
- Team leader: Damien Doligez, researcher at INRIA Paris-Rocquencourt.
- Project summary: TLA+ is a high-level mathematical language for specifying algorithms, protocols, or high-level views of systems. There is a model checker for TLA+ specifications, but in many cases, model checking cannot provide the desired level of confidence, and the only way to provide such confidence is with a rigorous proof. The goal of the project is to extend TLA+ with a language for writing formal proofs and to build a system for checking those proofs.
- Progress achieved: The extended language and its parser have been completed, and the proof checker is being built. The provers initially supported are Zenon, built by Doligez, and Isabelle.
- Comment: “The proof checker,” says team member Leslie Lamport, a principal researcher at Microsoft Research Silicon Valley, “consists of a proof manager that translates proof obligations into the language and logic of existing theorem provers and sends them to those provers to be checked. Although the system does not yet handle significant parts of the TLA+ language, it has reached the point where it can be used to check proofs of interesting algorithms. It is performing well, and I expect we will meet our goal of the public release of a useful system this fall.”
Secure Distributed Computations and Their Proofs
- Started: September 2006.
- Team leader: Cédric Fournet, senior researcher at Microsoft Research Cambridge.
- Project summary: The team develops formal tools for programming distributed computation with effective security guarantees. The goal is to enable programmers to express and prove high-level security properties with a reasonable amount of effort, sometimes automatically, sometimes with mechanical assistance.
- Progress achieved: Programming abstractions for security have been explored, implemented, and verified. This enhanced understanding of the relation between cryptography and formal proofs.
- Comment: “Our project involves 16 researchers, including four Ph.D. students,” Fournet says. “As a result of our research, we published 18 papers in international conferences and journals. We also prototyped and released a series of tools for secure distributed programming, including a cryptographic protocol compiler for multiparty sessions, a first-verified reference implementation for the TLS Internet standard, and a first machine-checked formalization of game-based computational cryptography, in Coq.”
TRACK B: COMPUTATIONAL SCIENCES AND SCIENTIFIC INFORMATION INTERACTION
Dynamic Dictionary of Mathematical Functions
- Started: Fall 2007.
- Team leader: Bruno Salvy, scientific leader of the INRIA project team ALGO.
- Project summary: The project aims to automate the computation of numerous mathematical formulae needed in analysis, with the intent of demonstrating that large parts of the code dealing with elementary and special functions in computer algebra systems can be generated automatically in a uniform manner.
- Progress achieved: An original prototype of the Dynamic Dictionary of Mathematical Functions is available on the Web. Its engine is based on a new representation of special functions of mathematics using linear differential equations as a data structure, instead of the more traditional tree-based approach, and its GUI works with standard Internet navigators.
- Started: December 2007.
- Team co-leaders: Jean-Daniel Fekete, scientific leader of the INRIA project team AVIZ, and Wendy Mackay, scientific leader of the INRIA project team IN-SITU.
- Project summary: The team’s research goal is to help researchers capture, visualize, and interact with their own and their colleagues’ activities over time. Increasing researchers’ awareness of their activities would improve not only productivity, but also their creativity and understanding.
- Progress achieved: Members of the INRIA IN-SITU team, Microsoft Research Redmond’s Visualization and Interaction Research Group (VIBE), and the IN-SITU spinoff AVIZ have been collaborating in various forums, and several prototypes have been completed related to the capture of temporal data and the development of a data-exchange model.
- Comment: “We want to provide Wikipedians with a better awareness of their group activities,” says Mary Czerwinski, research-area manager of VIBE. “INRIA has collected and processed data on article revisions from Wikipedia. Each team from Microsoft Research and INRIA has been designing and developing novel visualizations to enable people to explore and understand the collaborative activity on Wikipedia. This has been a very successful collaboration, because we share the data and we learn from each other’s experience, which help us build better visualizations to bring patterns of interest to light.”
Adaptive Combinatorial Search for E-Science
- Started: Fall 2007.
- Team co-leaders: Youssef Hamadi, researcher at Microsoft Research Cambridge, and Marc Schoenauer, co-scientific leader of the INRIA project team TAO.
- Project summary: This work aims to improve the applicability of constraint-based or heuristic-based solvers to complex scientific problems. E-scientists use search to tackle a variety of important problems but encounter limitations of current solving technologies poorly adapted to these new domains.
- Progress achieved: The team’s combination of expertise in constraint programming, evolutionary algorithms, and machine learning has led to original results in learning how to choose the best heuristic at any node of a search tree and in using Multi-Armed Bandit algorithms for operator selection. The ideas of CMA-ES, the state-of-the-art method in evolutionary continuous optimization, have been extended to any other search algorithm and to multiobjective optimization.
- Comment: “The difficulties faced by the users of combinatorial search techniques arise mainly from the significant range of algorithms and/or parameter choices involved when using this type of approach,” Hamadi says, “and the lack of guidance as to how to proceed for selecting them. The goal of our project is to improve the applicability of these techniques by letting them adapt automatically to the particularities of a given problem. After one year, the project has developed several new adaptive techniques leading to 3 software components, 11 publications, and 6 invited tutorials.”
Image and Video Mining for Science and Humanities
- Started: Sept. 15, 2008.
- Team leader: Jean Ponce, scientific leader of the INRIA project team WILLOW.
- Project summary: Scientific Image and Video Data Mining is the first of several projected inquiries for this project. The team is addressing problems of mining dynamical remote date with applications in computational ecology and environmental science; mining historical collections of photographs and paintings with applications to archaeology and culture-heritage preservation; and mining TV broadcasts with applications to sociology.
- Progress achieved: This is the newest of the Joint Centre projects, having been in existence just five months, but the team holds great promise, including as it does some of the world’s pre-eminent experts in computer vision.
- Comment: “The most recent theme in the MSR-INRIA collaboration addresses image and video mining,” says Andrew Blake, deputy managing director of Microsoft Research Cambridge.”It brings together three of INRIA's labs that have world-class facilities in computer vision, those in Paris, Grenoble, and Rennes. The aim is to bring the machine-learning discipline of data-rich computing to bear in building powerful systems for analysis of rich visual media.”