Logiciels Et Mathématiques M E

en Français

Home Team Software Internship Activity reports Actions AOC , S-Java, Modocop, and Concert Seminar

Formal methods to construct safe software. The aim of the Lemme project is to introduce and develop the usage of formal methods to construct safe software. We particularly address scientific computing software (computer algebra, computer arithmetics) and software for smart cards. The project develops methods and tools to help in producing correct programs from mathematical descriptions of data, algorithms, programming languages, their properties and the proofs of these properties. Our privileged tool is the Coq system (developed by the Démon team at University of Paris-Sud and the Logical, project at INRIA Rocquencourt). Research topics: Proof environments Formal presentation of mathematics and type theory Certified algorithms Programming language semantics Scientific collaboration: TYPES Working Group: computer assisted reasoning based on type theory. Cooperative Research Initiatives: AOC (Certified computer arithmetics) , S-Java (Combination of formal tools for verifying security properties of Java programs). Mowgli (European LTR project): formal mathematics on the Web (Universities of Bologna, Berlin, Nijmegen, Eindhoven, DFKI Saarbrücken, Max Planck Institute, and Trusted Logic) University of Nice, laboratoire A.Dieudonné: formalizing schemas in algebraic geometry. University of Minho: type theory University of the Republic (Uruguay) and University of Cordoba (Argentina): formal methods for smart cards. Industrial Collaborations: European project Verificard: modeling and verifying the JavaCard platform and programs written in this language (GemPlus, Bull, Universities of Nijmegen, Munich, Hagen, Sics). Dassault: handling well-founded recursion in Coq.

Contact: Loic.Pottier@sophia.inria.fr or Yves.Bertot@sophia.inria.fr .

Updated: 22-10-2001