Séance de cours

Vérification des compilateurs : défis et avantages

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Description

Cette séance de cours de l'instructeur explore les défis et les avantages de la vérification du compilateur, en mettant l'accent sur la vérification formelle des compilateurs pour les logiciels de haute assurance. La séance de cours se penche sur l'histoire de la vérification du compilateur, les subtilités de l'optimisation du compilateur, et la nature délicate de la génération de code. Il examine l'importance de vérifier les compilateurs pour les logiciels critiques, le concept de compilateurs vérifiés et l'impact des bogues de mauvaise compilation. La séance de cours couvre également le projet CompCert, qui vise à développer et prouver correctement un compilateur réaliste pour les logiciels embarqués critiques. Au moyen d'exemples et d'études de cas, la séance de cours souligne l'importance de la vérification formelle pour assurer la fiabilité et la sécurité des compilateurs.

Source officielle

Proximité ontologique

Génie informatique

Programmation informatique: Compilateur

Concepts associés (32)

Software verification and validation

In software project management, software testing, and software engineering, verification and validation (V&V) is the process of checking that a software system meets specifications and requirements so that it fulfills its intended purpose. It may also be referred to as software quality control. It is normally the responsibility of software testers as part of the software development lifecycle.

Compilateur

En informatique, un compilateur est un programme qui transforme un code source en un code objet. Généralement, le code source est écrit dans un langage de programmation (le langage source), il est de haut niveau d'abstraction, et facilement compréhensible par l'humain. Le code objet est généralement écrit en langage de plus bas niveau (appelé langage cible), par exemple un langage d'assemblage ou langage machine, afin de créer un programme exécutable par une machine.

Vérification formelle

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Qualité logicielle

En informatique et en particulier en génie logiciel, la qualité logicielle est une appréciation globale d'un logiciel, basée sur de nombreux indicateurs. La complétude des fonctionnalités, la correction et précision des résultats, la fiabilité, la tolérance de pannes, la facilité et la flexibilité de son utilisation, la simplicité, l'extensibilité, la compatibilité et la portabilité, la facilité de correction et de transformation, la performance, la cohérence et l'intégrité des informations qu'il contient sont tous des facteurs de qualité.

Assurance qualité

On désigne par assurance qualité un moyen d'obtenir confiance dans l'assurance de la qualité c'est-à-dire dans l'aptitude de la société ou de l'organisation à satisfaire le niveau de qualité désiré. Le terme « assurance qualité » qui élide les articles naturellement présents dans la langue française est très commun du fait que le concept a été importé (anglicisme) de la langue anglaise où l'on parle de Quality assurance. Le terme assurance a donc ici la valeur de confiance que lui donne la langue anglaise.

Afficher plus

Séances de cours associées (64)

Architectures VLIW: Compilateurs et parallélisme de niveau d'instruction

Couvre les architectures et les compilateurs VLIW, en se concentrant sur le parallélisme de niveau d'instruction et les techniques d'optimisation.

Exactitude des compilateurs: Partie 1

Explore l'exactitude du compilateur, des exemples de compilateurs vérifiés, la vérification formelle et les défis des compilateurs de certification.

Analyse statique pour Amy: Techniques et Implémentations

Explore les techniques d'analyse statique comme l'analyse basée sur l'AST et l'analyse des taints appliquée au langage Amy.

Compilateurs : défis avec les processeurs de signaux numériques

Couvre les défis de la compilation pour les processeurs de signaux numériques en raison de leurs caractéristiques architecturales uniques et des irrégularités.

Compiler Extension Lab

Couvre le Compiler Extension Lab, en se concentrant sur l'ajout de nouvelles fonctionnalités à un compilateur de langage fonctionnel simple.

Afficher plus

Concepts associés (32)

Software verification and validation

Compilateur

Vérification formelle

Qualité logicielle

Assurance qualité

Afficher plus