Verifying the LLVM

Explore the Verified LLVM (Vellvm) project in this 40-minute Strange Loop Conference talk. Dive into the semantics of LLVM code and learn how to ensure LLVM-based tools perform as intended, especially for safety-critical applications. Examine the LLVM intermediate representation from a programming language semantics perspective and discover how Vellvm provides a foundation for developing machine-checkable formal properties about LLVM IR programs and transformation passes. Gain insights into LLVM code structure, including its more complex aspects, and understand how modern interactive theorem provers like Coq can verify compiler transformations. No prior experience with LLVM or formal verification technologies is required. The talk covers LLVM Intermediate Representation, compiler infrastructure, undef and optimization interactions, compiler bugs, deep specifications, the CompCert inspiration, Vellvm framework, LLVM IR semantics, writing interpreters in Coq, interaction trees, mem2reg register promotion, and getting started with Coq.

Intro
Collaborators
PLAN • LLVM Intermediate Representation
LLVM Compiler Infrastructure
Other LLVM IR Features
But... it's complex
One Example: undef
Interactions with Optimizations
What's the problem?
Compiler Bugs
Deep Specifications
Inspiration: CompCert
The Vellvm Project
Vellvm Framework
LLVM IR Semantics
Writing Interpreters in Coq
Interaction Trees
LLVM Interpreter in Cog
mem2reg register promotion
Caveats
Getting started with Cog