Vellvm – Verifying the LLVM

  • Date Friday, July 13, 2018  Time 11:00 AM
  • Speaker Steve Zdancewic
  • Location Galois Inc., 421 SW 6th Ave. Suite 300, Portland, OR, USA, (3rd floor of the Commonwealth building)
  • Galois is pleased to host the following tech talk.
    These talks are open to the interested public--please join us!
    (There is no need to pre-register for the talk.)

    This talk will also be live streamed on our YouTube channel


In this talk, I’ll give a high-level overview of Penn’s Vellvm (Verified LLVM) project, which aims to build formal semantics in Coq for the LLVM IR. I’ll sketch some of our past results, in which we verified memory safety transformations and a variant of LLVM’s mem2reg optimization, focusing on the structure of the proof techniques.  Along the way, I’ll highlight some of the challenges of reasoning about LLVM code (many of which are still open issues). I’ll wrap up with a status report about our ongoing efforts to re-engineer Vellvm as part of the DeepSpec NSF Expeditions project.
No experience with LLVM or Coq will be assumed.


I study programming languages and computer security. I have wide-ranging interests, and some of my most recent work touches on: Coq verification of LLVM program transformations and randomized algorithms, type-directed program synthesis, linear types and GUI programming. I have also spent a lot of time thinking about language-based enforcement of information-flow policies, low-level code memory safety, understanding dynamic security policies, and authorization logic. I am also interested in secure concurrent and distributed computing, functional programming languages, type theory, linear and modal logics, theorem proving and mechanized metatheory.