This HTML5 document contains 65 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dcthttp://purl.org/dc/terms/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
n16http://g.co/kg/m/
dbpedia-ruhttp://ru.dbpedia.org/resource/
schemahttp://schema.org/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n4https://github.com/AbsInt/
category-frhttp://fr.dbpedia.org/resource/Catégorie:
n12http://fr.dbpedia.org/resource/Modèle:
wikipedia-frhttp://fr.wikipedia.org/wiki/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
dbpedia-frhttp://fr.dbpedia.org/resource/
prop-frhttp://fr.dbpedia.org/property/
provhttp://www.w3.org/ns/prov#
xsdhhttp://www.w3.org/2001/XMLSchema#
dbrhttp://dbpedia.org/resource/
wikidatahttp://www.wikidata.org/entity/

Statements

Subject Item
dbpedia-fr:CompCert
rdf:type
schema:CreativeWork wikidata:Q386724 owl:Thing wikidata:Q7397 dbo:Software dbo:Work
rdfs:label
CompCert CompCert
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.
owl:sameAs
dbpedia-ru:CompCert n16:0bxzkh3 dbr:CompCert wikidata:Q5155256
dbo:wikiPageID
6888726
dbo:wikiPageRevisionID
183396359
dbo:wikiPageWikiLink
dbpedia-fr:Bug_(informatique) dbpedia-fr:OCaml dbpedia-fr:X64 dbpedia-fr:C_(langage) dbpedia-fr:Xavier_Leroy dbpedia-fr:X86 dbpedia-fr:Coq_(logiciel) dbpedia-fr:Compilateur dbpedia-fr:Méthode_formelle_(informatique) dbpedia-fr:Langage_machine dbpedia-fr:GNU_Compiler_Collection category-fr:Assistant_de_preuve dbpedia-fr:Architecture_ARM category-fr:Compilateur_C dbpedia-fr:Vérification_formelle dbpedia-fr:Institut_national_de_recherche_en_informatique_et_en_automatique dbpedia-fr:PowerPC dbpedia-fr:Logiciel_multiplateforme dbpedia-fr:Architecture_de_processeur dbpedia-fr:RISC-V
dbo:wikiPageExternalLink
n4:CompCert
dbo:wikiPageLength
3242
dct:subject
category-fr:Assistant_de_preuve category-fr:Compilateur_C
prop-fr:wikiPageUsesTemplate
n12:Portail n12:Infobox_Logiciel n12:Références n12:Ébauche n12:Date
prov:wasDerivedFrom
wikipedia-fr:CompCert?oldid=183396359&ns=0
prop-fr:type
dbpedia-fr:Compilateur
prop-fr:dateDePremièreVersion
2008-04-03
prop-fr:langageDeProgrammation
dbpedia-fr:OCaml dbpedia-fr:Coq_(logiciel)
prop-fr:licence
INRIA Non-Commercial License Agreement
prop-fr:développeurs
dbpedia-fr:Institut_national_de_recherche_en_informatique_et_en_automatique dbpedia-fr:Xavier_Leroy
prop-fr:environnements
dbpedia-fr:Logiciel_multiplateforme
prop-fr:dépôt
n4:CompCert
prop-fr:exécutable
ccomp
foaf:isPrimaryTopicOf
wikipedia-fr:CompCert
dbo:releaseDate
2008-04-03
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.
dbo:license
wikidata:Q94920209
dbo:operatingSystem
dbpedia-fr:Logiciel_multiplateforme
dbo:programmingLanguage
dbpedia-fr:OCaml dbpedia-fr:Coq_(logiciel)
dbo:publisher
dbpedia-fr:Institut_national_de_recherche_en_informatique_et_en_automatique dbpedia-fr:Xavier_Leroy
dbo:type
dbpedia-fr:Compilateur