

Computer aided verification of
proofs and software.
The goal of the the Marelle project is to study and use
techniques for verifying mathematical proofs on the computer to
ensure the correctness of software. The targeted domains consist
in software for scientific computation (computer algebra, computer
aritmetics). The project develops methods and tools to help producing
correct program from precise descriptions of the data, the algorithms,
their properties, and the proofs of these properties.
Main research directions:
 Proof working environments
 Formalizations of mathematics and type theory
 Certified algorithms
 Formal properties of numbers, exact computation.
Scientific collaborations:
 types working
group: computerassisted reasoning based on type theory.
 Cooperative research actions: AOC
(Arithmétique des ordinateurs certifiée, certified computer arithmetics), Concert (certified
compiler)
 Projet Mowgli (European LTR project): Formal mathematics on the worldwide web
(Universities of Bologna, Berlin,
Nijmegen, Eindhoven, DFKI Saarbrücken, Max Planck
Institute, and Trusted Logic)
 University of Nice, laboratoire A.Dieudonné, formalisation of proofs
in mathematics (esp. algebraic geometry).
Potential applications:
Formal verification for the following aspects of software:
 software controlling physical devices
(transportation, medical robotics, satellite position control),
 compilers for specialpurpose languages,
 highprecision for floatingpoint number computations,
 Evaluation of erreur probability for software systems.
