|
Domaine de Voluceau, 78153 Rocquencourt Cedex, France
Visit the institution home page.
Site responsible: Prof. Hugo Herbelin.
INRIA (National Institute for Research in Computer Science and Control) is a French public-sector scientific and technological institute operating under the dual authority of the Ministry of Research and the Ministry of Industry. INRIA's missions are ``to undertake basic and applied research, to design experimental systems, to ensure technology and knowledge transfer, to organise international scientific exchanges, to carry out scientific assessments, and to contribute to standardisation''.
The research carried out at INRIA brings together experts from the fields of computer science and applied mathematics covering the following areas: Networks and Systems; Software Engineering and Symbolic Computing; Man-Machine Interaction; Image Processing, Data Management, Knowledge Systems; Simulation and Optimisation of Complex Systems.
INRIA gathers in its premises around 2 100 persons including 1 600 scientists , many of which belong to partner organisations (CNRS, industrial labs, universities) and are assigned to work in common ``projects''. On INRIA's budget, around 500 full-time equivalent R&D positions can be accounted for.
A large number of INRIA senior researchers are involved in teaching and their PhD students (about 550) prepare their thesis within the different INRIA research projects (currently 74).
Its budget is roughly 90 MEuro, 20% of which comes from research and development contracts, royalties and sales. Industrial relations are strategic for INRIA:
INRIA is a member of ERCIM EEIG, European Research Consortium for Computer Science and Mathematics. Outside Europe, INRIA also has a significant activity: it has created joint research laboratories (Russia and China), signed cooperation agreements (NSF, India, Brazil, etc.) and promotes intensive scientific exchanges.
Members of the project also involved in MOWGLI:
The purpose of the Lemme project is to introduce and develop formal methods for use in writing scientific computing software. In scientific computing, algorithms and mathematics are at the forefront. We are thus developing tools and methods to help producing correct programs starting from the usual mathematical descriptions of data, algorithms, properties and proofs, structured into four research themes:
The project belongs to the European working group Types, and to the French action AOC (Arithm\'etique des Ordinateurs Certifiée). It keeps up industrial collaborations with Dassault-Aviation (program proof environments), Alcatel Space Industry (certified numerical code), and GemPlus (Javacard certification), and also collaborates with teachers at university on the use of formal proofs and Web-based environments in mathematics courses.
Members of the project also involved in MOWGLI:
The LogiCal team of INRIA is working on theoretical and practical aspects of mathematical proofs. It develops the Coq proof assistant, an implementation of an expressive formalism called Calculus of Inductive Constructions. Coq is used both for development of formal mathematics and for certification of programs, especially protocols and critical systems.
The LogiCal project is a joint project with University Paris 11. It is involved in the European TYPES working group and in several French actions. Especially, it is involved in the S-Java action aiming at certifying safety properties for JavaCard programs, in a project aiming at certifying algorithms used in computer algebra systems. LogiCal collaborates also on proof automation with France Telecom.
This page is hosted by the
Department of Computer Science,
University of Bologna.
Last updated Fri Feb 2 17:12:28 CET 2007. |
|