Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Compiler verification: Challenges and Benefits

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)

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.

Optimizing compiler

In computing, an optimizing compiler is a compiler that tries to minimize or maximize some attributes of an executable computer program. Common requirements are to minimize a program's execution time, memory footprint, storage size, and power consumption (the last three being popular for portable computers). Compiler optimization is generally implemented using a sequence of optimizing transformations, algorithms which take a program and transform it to produce a semantically equivalent output program that uses fewer resources or executes faster.

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.

Bootstrapping (compilers)

In computer science, bootstrapping is the technique for producing a self-compiling compiler – that is, a compiler (or assembler) written in the source programming language that it intends to compile. An initial core version of the compiler (the bootstrap compiler) is generated in a different language (which could be assembly language); successive expanded versions of the compiler are developed using this minimal subset of the language.

Formal methods

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Related lectures (31)

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.

Verifying Compiler: Spec# Approach

Explores the Spec# programming system, focusing on a verifying compiler for C# 2.0.

Compiler Extension Lab

Covers the Compiler Extension Lab, focusing on adding new functionality to a simple functional language compiler.

Code Generation Lab