Inria
Inria.fr
Inria Channel
- Presentation
- HAL publications
- Activity reports
MARELLE Research team
Mathematical, Reasoning and Software
- Leader : Yves Bertot
- Type : Project team
- Research center(s) : Sophia
- Field : Algorithmics, Programming, Software and Architecture
- Theme : Programs, Verification and Proofs
Team presentation
The goal of the MARELLE project-team 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-team 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.Research themes
- Proof development environments
- Formalization of mathematics and type theory
- Certified software
- Formal properties of numbers, exact arithmetics
International and industrial relations
- ANR Galapagos: Geometry, Algorithms, Proofs
- ANR Compcert: certified compiler
- ANR A3Pat: collaboration between rewriting and proving
- Microsoft-INRIA Institute: Mathematical components
- TYPES Working Group: computer-assisted reasoning based on type theory.
- University of Nice, A.Dieudonné Laboratory: formalization of proofs in mathematics
Keywords: Formalization of mathematical algorithms Computer assisted proof
Research teams of the same theme :
- ABSTRACTION - Abstract Interpretation and Static Analysis
- ATEAMS - Analysis and Transformation based on rEliAble tool coMpositionS
- CARTE - Theoretical adverse computations, and safety
- CASSIS - Combination of approaches to the security of infinite states systems
- CELTIQUE - Software certification with semantic analysis
- COMETE - Concurrency, Mobility and Transactions
- CONTRAINTES - Constraint programming
- DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
- FORMES - Formal Methods for Embedded Systems
- GALLIUM - Programming languages, types, compilation and proofs
- MEXICO - Modeling and Exploitation of Interaction and Concurrency
- MOSCOVA - Mobililty, security, concurrence, verification and analysis
- PAREO - Formal islands: foundations and applications
- PARSIFAL - Proof search and reasoning with logic specifications
- PI.R2 - Design, study and implementation of languages for proofs and programs
- PROSECCO - Programming securely with cryptography
- SECSI - Security of information systems
- TASC - Theory, Algorithms and Systems for Constraints
- TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
- TYPICAL - Types, Logic and computing
- VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Contact
Team leader
Yves Bertot
(See all teams)
Tel.: +33 4 92 38 77 39
Secretariat
Tel.: +33 4 92 38 76 00
Find out more
Genealogy
This team follows
See also
