Séminaire Cambium, Inria Paris
                                 Amphi Lions
                           Vendredi 10 avril, 10h30

                               Steve Zdancewic
                          University of Pennsylvania

                 Vellvm: Formal Verification of LLVM IR Code

LLVM is an industrial-strength compiler that's used for everything from iOS
development to academic research. However, like any piece of complicated
software, LLVM IR itself has a complex specification, making it hard to fully
understand, and its implementation has bugs, which can cause potentially
catastrophic mis-compilation errors. These properties make the LLVM framework a
sweet spot for bug-finding and verification technologies--any improvements to it
are amplified across its many applications.

This talk will survey the Vellvm (Verified LLVM) project, which aims to define a
formal, mathematical specification for a large, useful subset of LLVM. Vellvm is
implemented in the Rocq interactive theorem prover, which can be used for
developing machine-checkable properties about LLVM IR programs and compiler
optimization passes. Along the way, we'll explore some subtleties of LLVM IR
semantics and see how Vellvm models them in a modular way by composing "monadic
interpreters" built on top of a data structure called interaction trees.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.