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.
- types working
group: computer-assisted reasoning based on type theory.
- Cooperative research actions: AOC
(Arithmétique des ordinateurs certifiée, certified computer arithmetics), Concert (certified
- 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).
Formal verification for the following aspects of software:
- software controlling physical devices
(transportation, medical robotics, satellite position control),
- compilers for special-purpose languages,
- high-precision for floating-point number computations,
- Evaluation of erreur probability for software systems.