Marelle

Mathematics
A
Reasoning
E
L (and software)
L
E

Home

Team members

Software

Internships

Activity reports

Actions
AOC , Concert

Seminar

Bibliography

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: computer-assisted 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 special-purpose languages,

high-precision for floating-point number computations,

Evaluation of erreur probability for software systems.

Contact: Yves.Bertot@sophia.inria.fr