The research activities of the
joint INRIA-Microsoft Research Centre is structured around two paths of research
: formal methods and the IT tools for science.
Three research projects into formal methods started in 2006.
Three projects were started in 2006 with the goal to contribute to the
progress of programming languages and to research the way in which software
code is designed using mathematical methods, instead of the empirical methods
based on know-how and experience, that are generally referred to as software
engineering. The purpose of this initiative is to improve quality, reliability
and security.
Former INRIA Chairman, Gilles Kahn, who died in 2006, was a very keen supporter
of this cooperation with Microsoft and was one of the main driving forces
behind the cooperation in this field.
Project for secure distributed calculation and formal evidence
Main research engineers:
• Cedric Fournet (Microsoft Research)
• James Leifer (INRIA)
Over the past 10 years, demands for security have risen and the need for
secure codes has increased and become more complex. A significant part of
programming now affects the security of information systems. Programmers
now focus on guaranteeing and analyzing security issues. This project includes
plans to design formal tools for the simple programming of distributed calculations
that include security guarantees. The goal is to enable programmers to express
and prove the correction properties at a reasonable effort, that may be
automatic or partly manual, as part of the program development process.
Mathematic Components Project
Main research engineers:
• Georges
Gonthier (Microsoft Research)
• Benjamin
Werner (INRIA)
The purpose of this project is to prove that formal mathematical theories
can be built from components, just like modern software. The term "component" is
understood as a module that defines both the static aspects (objects and
proposals) and the dynamic aspects (evidence and calculation methods) of
a theory. In this case, the proposal consists in developing a general platform
for mathematical components that is built on the Coq extension used to demonstrate
the four-color theorem. The platform will be validated by two significant
developments: an effective theory of the arithmetic and proof of the Feit-Thompson
theorem. The first project could even be used to solve the various remarkable
challenges posed by mathematical formalization, including the demonstration
by Coq of Hale's proof of the Kepler conjecture. The second project will
be a decisive step towards creating a large-scale collaborative effort to
take up a new challenge in the field of formal proof: the classification
of simple finite groups.
The Tools and Methodologies project for formal specification and proof
Main research engineers:
• Damien
Doligez (INRIA)
• Stephan Merz (INRIA)
• Leslie Lamport (Microsoft Research)
The purpose of this project is to build a system capable of mechanically
verifying the proof of systems specified in TLA+. TLA+ is a formal, very
high-level language used to specify algorithms and systems. This language
uses the usual mathematical bases, such as the theory of ensembles, as taught
in secondary schools or used by Bourbaki. TLA+ has its own model checker
that is used to finalize the TLA+ specifications. However, the numerous
specifications are too complex to be checked by sufficiently large models
required to detect the most subtle errors. In most cases, the model checks
do not offer the levels of trust required for critical applications. Machine-proven
mathematical proof can solve these problems by guaranteeing that the specification
checks the announced properties of every model, irrespective of their size
and even if they are infinite.
The scientific challenge: This path of research focuses on
significantly improving the actual and perceived quality of software and
proving that information technology can also demonstrate mathematical theorems
that have been waiting to be proven for centuries (also
known as conjectures).
In 2005, Georges Gonthier demonstrated the 4-color theorem, that had been
waiting for an irrefutable demonstration for 150 years. Now, he plans to
address the Kepler conjecture in the same manner. The Kepler conjecture
applies to the packing of spheres, or cannon balls, in a minimal volume.
This conjecture was demonstrated by Hales in 2003 and did not even respect
the criteria of the mathematicians. The conjecture states that the stacking
of the spheres in the densest possible space corresponds to the face-centered
cubic surface (see
the crystalline system). This conjecture had been waiting
to be proved for more than 350 years!
The second path of research is the IT tools for science.
A number of projects will be started up in 2007 as part of this
research effort, including the "Re-Activity" project, which will
be presented at the inauguration and is the
result of the cooperation between
Wendy
MacKay and Mary
Cswersinsky,
a senior Microsoft research engineer in Redmond, USA .
