Next: Grenoble
Up: Cooperating sites
Previous: Edinburgh


France Telecom R&D

The Formal Methods Group in FT R&D participated in the previous EU funded TYPES working group. It has long experience in using logic based formalisms, including type theory, in a number of telecommunication applications: communication protocols, cryptographic protocols, embedded platforms. It has experience using various proof systems and verification tools, e.g. HOL, PVS, Coq, B-tools, SMV and Kronos.

The group will mainly contribute to the objective of Correctness of Computer Systems through its work on programming with dependent types, static analysis, deduction systems and interfaces between them. Some application fields which are considered are modelling communicating systems over cellular networks and verification of security properties.

The Formal Methods Group contributed actively to the development of the Coq system through a number of contributed theories, tactics (Presburger arithmetic, binary arithmetic, rewriting) and other tools, such as the experimental Coq-ELAN interface. The group has sustained relationship with national projects LOGICAL, PROTHEO, LEMME and LANDE at INRIA, and the Demons group at LRI-Paris Sud. It was also an end-user panel member of the Verificard IST.

The senior members of the group involved in TYPES are



Bengt Nordström 2005-09-22