Home

Collaborations

Contracts

  • The INRIA ARC Corias about the conception of proof assistants based on superdeduction modulo.
  • The joint European research project MOWGLI on development and management of mathematical documents on the Web.
  • Certified code generation for object oriented applications: Geccoo.
  • Modulogic: creation of a tool for certified software generation.
  • Analysis and Verification for the Reliability Of Embedded Systems: Averroes
  • TYPES is a working group in the ESPRIT program of the European Union.
  • Some members of the TypiCal project participate to the Mathematical Components project within the INRIA-Microsoft Research joint centre.

Teams

  • The Lemme project in Sophia-Antipolis develops formal methods to do program proofs.
  • In Nancy, the Protheo project aims at designing and implementing tools for program specification and verification, incorporating constraint solving and term rewriting techniques.
  • The SPI project at LIP6 (Paris) deals with programmation and more precisely with semantics, proofs and implementation issues.
  • The Foundations group in Nijmegen, the Netherlands, studies mathematical theories concerned with computability, provability and complexity.
  • NIA is a research institute for the aerospace and atmospheric fields. It hosts a Formal Methods group working tightly with scientists at the NASA Langley Research Center.