| Property |
Value |
| dbo:abstract
|
- 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 C90 / ANSI C avec quelques limitations mineures et plusieurs extensions inspirées des normes ultérieures) entièrement écrit et prouvé avec le logiciel Coq. Le développeur principal est Xavier Leroy. 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. (fr)
- 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 C90 / ANSI C avec quelques limitations mineures et plusieurs extensions inspirées des normes ultérieures) entièrement écrit et prouvé avec le logiciel Coq. Le développeur principal est Xavier Leroy. 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. (fr)
|
| dbo:license
| |
| dbo:operatingSystem
| |
| dbo:programmingLanguage
| |
| dbo:publisher
| |
| dbo:releaseDate
| |
| dbo:type
| |
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 3242 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| prop-fr:dateDePremièreVersion
| |
| prop-fr:dépôt
| |
| prop-fr:développeurs
| |
| prop-fr:environnements
| |
| prop-fr:exécutable
| |
| prop-fr:langageDeProgrammation
| |
| prop-fr:licence
|
- INRIA Non-Commercial License Agreement (fr)
- INRIA Non-Commercial License Agreement (fr)
|
| prop-fr:type
| |
| prop-fr:wikiPageUsesTemplate
| |
| dct:subject
| |
| rdf:type
| |
| rdfs:comment
|
- 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 C90 / ANSI C avec quelques limitations mineures et plusieurs extensions inspirées des normes ultérieures) entièrement écrit et prouvé avec le logiciel Coq. Le développeur principal est Xavier Leroy. 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. (fr)
- 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 C90 / ANSI C avec quelques limitations mineures et plusieurs extensions inspirées des normes ultérieures) entièrement écrit et prouvé avec le logiciel Coq. Le développeur principal est Xavier Leroy. 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. (fr)
|
| rdfs:label
|
- CompCert (en)
- CompCert (fr)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:wikiPageWikiLink
of | |
| is oa:hasTarget
of | |
| is foaf:primaryTopic
of | |
