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).