Metraipolis › archive › dc_71feaacea36b

CompCert — Wikipedia (fr)

Source: Wikipedia (fr)
Original: https://fr.wikipedia.org/wiki/CompCert
License (as archived): CC-BY-SA-4.0
Archived: 2026-11-05T08:35:17.799Z
SHA-256 of the archived text: f93a24109a55d6e4a8494b6d58616c64398c7ac75ece1c69ad42ffddba4f3cff
Stable URL of this page: https://metraipolis.com/documento/dc_71feaacea36b

How to cite

CompCert — Wikipedia (fr) — Wikipedia (fr), https://fr.wikipedia.org/wiki/CompCert (CC-BY-SA-4.0); archived copy: https://metraipolis.com/documento/dc_71feaacea36b (Metraipolis archive dc_71feaacea36b, sha256 f93a24109a55d6e4a8494b6d58616c64398c7ac75ece1c69ad42ffddba4f3cff)

BibTeX

@misc{dc71feaacea36b,
  title = {CompCert — Wikipedia (fr)},
  howpublished = {Wikipedia (fr)},
  url = {https://fr.wikipedia.org/wiki/CompCert},
  note = {License CC-BY-SA-4.0; archived copy https://metraipolis.com/documento/dc_71feaacea36b; sha256 f93a24109a55d6e4a8494b6d58616c64398c7ac75ece1c69ad42ffddba4f3cff},
  year = {2026}
}

Archived text

Reproduced under CC-BY-SA-4.0. Attribution: Wikipedia (fr), https://fr.wikipedia.org/wiki/CompCert. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

CompCert est un projet dont l'objectif est la réalisation de compilateurs certifiés formellement. Ce projet développe essentiellement un compilateur, CompCert C, pour le langage C (ISO C99 avec quelques limitations mineures et plusieurs extensions inspirées de la norme ISO C2011) entièrement écrit et prouvé avec le logiciel Rocq. Le développeur principal est Xavier Leroy. Sandrine Blazy, Zaynah Dargaye, Jacques-Henri Jourdan, Michael Schmidt, Bernhard Schommer, et Jean-Baptiste Tristan participent activement en tant que développeurs à ce projet. Ce compilateur possède une preuve vérifiée par machine que le code généré se comporte de la même manière que le code source. Il permet de générer du code machine pour les architectures de processeur PowerPC, ARM, RISC-V, x86 et x86-64.

Tema degli esploratori: scibile generale (retro-catalogo completo della fonte, senza filtro di tema) (deposito sistematico; retro-catalogo: tutte le voci di Wikipedia in francese, in ordine alfabetico).
Fonte: Wikipedia in francese, voce «CompCert» — https://fr.wikipedia.org/wiki/CompCert
Wikidata Q5155256: «formally verified C compiler» (dati Wikidata in CC0 1.0) — https://www.wikidata.org/wiki/Q5155256
Autori: i contributori di Wikipedia (cronologia: https://fr.wikipedia.org/wiki/CompCert?action=history).
Licenza: Creative Commons Attribuzione-Condividi allo stesso modo 4.0 (CC BY-SA 4.0) — https://creativecommons.org/licenses/by-sa/4.0/. Il riuso richiede attribuzione e stessa licenza.
Estratto dell'introduzione non modificato nel contenuto; revisione 240272393, consultata il 2026-11-05T08:32:19.127Z tramite l'API ufficiale di Wikipedia. Impronta SHA-256 dell'estratto: 1703958e6df5a063cbc2ce00daef6ea06db17bd63e55ace897c3812b82c3d770