|
Compilation vérifiée : vers du logiciel zéro défaut| title | Compilation vérifiée : vers du logiciel zéro défaut |
|---|
| start_date | 2024/11/26 |
|---|
| schedule | 18h |
|---|
| online | no |
|---|
| location_info | amphi 25 |
|---|
| summary | La vérification déductive permet d’avoir des garanties très fortes sur l’absence de bug dans les logiciels; elle est utilisée pour développer des logiciels embarqués critiques, où toute erreur peut compromettre des vies humaines ou avoir d’autres conséquences catastrophiques. La vérification étant effectuée au niveau source, le compilateur, logiciel complexe et point de passage obligé pour obtenir un code écrit dans un langage compréhensible par la machine mais bien plus primitif, devient un maillon faible dans la chaîne de production du logiciel. Aussi, vérifier le compilateur lui-même permet de garantir qu’aucune erreur n’est introduite lors de la compilation. Plus généralement, cette approche ouvre la voie à la vérification des outils informatiques participant à la production et à la vérification du logiciel. Cet exposé présente les défis sémantiques qu’il a fallu résoudre pour développer CompCert, le premier compilateur optimisant ciblant plusieurs architectures et utilisé dans l'industrie, qui soit doté d’une preuve mathématique de correction vérifiée par ordinateur. Cette preuve se fonde sur un raisonnement sur la sémantique des programmes observés, c’est-à-dire une définition mathématique du comportement de ces derniers. Le code produit par CompCert est garanti se comporter comme prescrit par la sémantique du programme source C. Ce niveau de confiance dans la correction de la compilation permet à CompCert de répondre aux plus hauts niveaux de fiabilité logicielle. |
|---|
| responsibles | NC |
|---|
Workflow history| from state (1) | to state | comment | date |
|---|
| submitted | published | | 2024/11/15 14:55 UTC |
| |
|