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.