Table des matières
21 relations: Architecture ARM, Architecture de processeur, Association for Computing Machinery, Bug (informatique), C (langage), Compilateur, Coq (logiciel), GNU Compiler Collection, Institut national de recherche en informatique et en automatique, Langage machine, Logiciel multiplateforme, Méthode formelle (informatique), OCaml, PowerPC, Prix ACM Software System, RISC-V, Sandrine Blazy, Vérification formelle, X64, X86, Xavier Leroy.
- Compilateur
- Méthode formelle
Architecture ARM
Les architectures ARM sont des architectures externes de type RISC 32 bits (ARMv1 à ARMv7) et 64 bits (ARMv8) (28 octobre 2011).
Voir CompCert et Architecture ARM
Architecture de processeur
Une architecture externe de processeurLes termes d'architectures interne et externe ont notamment été repris en 1998 dans le document de, titulaire de la Chaire des techniques fondamentales de l'informatique au CNAM.
Voir CompCert et Architecture de processeur
Association for Computing Machinery
L'ACM (en anglais « », littéralement « association pour les machines de calcul ») est une association internationale à but non lucratif fondée en 1947, la première à être vouée à l'informatique.
Voir CompCert et Association for Computing Machinery
Bug (informatique)
MacIntosh d'Apple. En informatique, un bug (prononcé en français: Prononciation en français européen retranscrite phonémiquement selon la norme API.) ou bogueRecommandé en France par la Délégation générale à la langue française et aux langues de France (DGLFLF), au Canada et en Belgique.
Voir CompCert et Bug (informatique)
C (langage)
C est un langage de programmation impératif, généraliste et de bas niveau.
Compilateur
En informatique, un compilateur est un programme qui transforme un code source en un code objet.
Coq (logiciel)
Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe de l’Inria au sein du laboratoire du CNRS et en partenariat avec l'École polytechnique, le CNAM, l'Université Paris Diderot et l'Université Paris-Sud (et antérieurement l'École normale supérieure de Lyon).
Voir CompCert et Coq (logiciel)
GNU Compiler Collection
, abrégé en GCC, est un ensemble de compilateurs créés par le projet GNU.
Voir CompCert et GNU Compiler Collection
Institut national de recherche en informatique et en automatique
L'Institut national de recherche en informatique et en automatique (Inria) est un établissement public à caractère scientifique et technologique français spécialisé en mathématiques et informatique, placé sous la double tutelle du ministère de l'Enseignement supérieur, de la Recherche et de l'Innovation et du ministère de l'Économie et des Finances.
Voir CompCert et Institut national de recherche en informatique et en automatique
Langage machine
Le langage machine, ou code machine, est la suite de bits qui est interprétée par le processeur d'un ordinateur exécutant un programme informatique.
Voir CompCert et Langage machine
Logiciel multiplateforme
Un logiciel multiplateforme est un logiciel conçu pour fonctionner sur plusieurs plateformes informatiques.
Voir CompCert et Logiciel multiplateforme
Méthode formelle (informatique)
En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l'aide de logique mathématique, sur un programme informatique ou du matériel électronique numérique, afin de démontrer leur validité par rapport à une certaine spécification.
Voir CompCert et Méthode formelle (informatique)
OCaml
OCaml, anciennement connu sous le nom d'Objective Caml, est l'implémentation la plus avancée du langage de programmation Caml, créé par Xavier Leroy, Jérôme Vouillon,, Didier Rémy et leurs collaborateurs en 1996.
Voir CompCert et OCaml
PowerPC
PowerPC, parfois abrégé PPC, est une gamme de microprocesseurs dérivée de l'architecture de processeur RISC POWER d'IBM, et développée conjointement par Apple, IBM et Freescale (anciennement Motorola Semiconducteurs).
Voir CompCert et PowerPC
Prix ACM Software System
Le prix ACM Software System ou, est attribué tous les ans depuis 1983 à une institution ou à une ou plusieurs personnes sélectionnée pour le développement d'un logiciel ayant eu une influence sur le long terme, qui s'est traduite par des contributions conceptuelles, commerciales, ou les deux.
Voir CompCert et Prix ACM Software System
RISC-V
RISC-V (prononcé en anglais « RISC five » et signifiant « RISC cinq ») est une architecture de jeu d'instructions (instruction set architecture ou ISA) RISC ouverte et libre, disponible en versions 32, 64 et 128 bits.
Voir CompCert et RISC-V
Sandrine Blazy
Sandrine Blazy est professeure d'informatique à l'université de Rennes, spécialiste de vérification formelle de programmes.
Voir CompCert et Sandrine Blazy
Vérification formelle
On parle de vérification formelle quand on utilise les techniques des méthodes formelles.
Voir CompCert et Vérification formelle
X64
x86-64, ou x64, est une extension du jeu d'instructions x86 d'Intel, introduite par la société AMD avec la gamme AMD64.
Voir CompCert et X64
X86
La famille x86 regroupe les microprocesseurs compatibles avec le jeu d'instructions de l'Intel 8086.
Voir CompCert et X86
Xavier Leroy
Xavier Leroy (né le) est un informaticien français, professeur au Collège de France et précédemment directeur de recherche à l'INRIA.
Voir aussi
Compilateur
- Binding
- Bootstrap (compilateur)
- C--
- CompCert
- Compilateur
- Compilation anticipée
- Compilation incrémentale
- Décompilateur
- Emscripten
- Free Pascal
- GNU Compiler Collection
- GnuCOBOL
- LLVM
- Moteur d'analyse de grammaire
- Nanoc
- SmartEiffel
- Test de Banerji (informatique)
- UWIN
- XcodeGhost
Méthode formelle
- Analyse temporelle statique
- Bisimulation
- CompCert
- Démonstration automatique de théorèmes
- E-LOTOS
- Fonction 91 de McCarthy
- Invariant de boucle
- Lambda-calcul
- Language Of Temporal Ordering Specification
- Lustre (langage)
- Méthode B
- Méthode formelle (informatique)
- Machine à états abstraits
- Machine de Turing
- Précondition
- Preuve assistée par ordinateur
- Principe de substitution de Liskov
- Problème SAT
- Sémantique algébrique (informatique)
- Sémantique des langages de programmation
- Sûreté de fonctionnement
- Satisfiability modulo theories
- Système asynchrone
- Système critique
- TLA+
- Théorie des ensembles
- Théorie des types homotopiques
- Vérification formelle
- Vienna Development Method