Lecture

Compiler verification: Challenges and Benefits

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Description

This lecture by the instructor explores the challenges and benefits of compiler verification, focusing on the formal verification of compilers for high-assurance software. The lecture delves into the history of compiler verification, the intricacies of compiler optimization, and the delicate nature of code generation. It discusses the importance of verifying compilers for critical software, the concept of verified compilers, and the impact of miscompilation bugs. The lecture also covers the CompCert project, which aims to develop and prove correct a realistic compiler for critical embedded software. Through examples and case studies, the lecture highlights the significance of formal verification in ensuring the reliability and safety of compilers.

Official source

Ontological neighbourhood

Computer engineering

Computer programming: Compilers

Related concepts (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.

Compiler

In computing, a compiler is a computer program that translates computer code written in one programming language (the source language) into another language (the target language). The name "compiler" is primarily used for programs that translate source code from a high-level programming language to a low-level programming language (e.g. assembly language, object code, or machine code) to create an executable program. There are many different types of compilers which produce output in different useful forms.

Formal verification

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.

Software quality

In the context of software engineering, software quality refers to two related but distinct notions: Software's functional quality reflects how well it complies with or conforms to a given design, based on functional requirements or specifications. That attribute can also be described as the fitness for purpose of a piece of software or how it compares to competitors in the marketplace as a worthwhile product. It is the degree to which the correct software was produced.

Quality assurance

Quality assurance (QA) is the term used in both manufacturing and service industries to describe the systematic efforts taken to assure that the product(s) delivered to customer(s) meet with the contractual and other agreed upon performance, design, reliability, and maintainability expectations of that customer. The core purpose of Quality Assurance is to prevent mistakes and defects in the development and production of both manufactured products, such as automobiles and shoes, and delivered services, such as automotive repair and athletic shoe design.

Related lectures (64)

VLIW Architectures: Compilers and Instruction Level Parallelism

Covers VLIW architectures and compilers, focusing on instruction level parallelism and optimization techniques.

Correctness of Compilers: Part 1

Explores compiler correctness, examples of verified compilers, formal verification, and the challenges of certifying compilers.

Static Analysis for Amy: Techniques and Implementations

Explores static analysis techniques like AST-based analysis and taint analysis applied to the Amy language.

Compilers: Challenges with Digital Signal Processors

Covers the challenges of compiling for digital signal processors due to their unique architectural features and irregularities.

Compiler Extension Lab