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 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 Coq 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
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_.
We'll also see some applications of Vellvm for verified compiler construction.

No experience with LLVM or formal verification technologies will be assumed.

BIO

Stephan A. Zdancewic, Ph.D. - 
Dr. Zdancewic is the Schlein Family President's Distinguished Professor and
Associate Department Chair in Computer and Information Science at the University
of Pennsylvania.  He received his Ph.D. in Computer Science from Cornell
University in 2002, and he graduated from Carnegie Mellon University with a
B.S. in Computer Science and Mathematics in 1996.  He is the recipient of an NSF
Graduate Research Fellowship, an Intel fellowship, an NSF CAREER award, and a
Sloan Fellowship.  His numerous publications in the areas of programming
languages and computer security include several best paper awards.

Dr. Zdancewic's research centers around using programming languages technology
to help build secure and reliable software.  He has worked on type-based
enforcement of both information-flow and authorization policies, compiler
techniques for ensuring memory safety of legacy C code, and, more recently, on
using interactive theorem-proving technology to construct highly-trustworthy
software systems. His interests also include type theory and linear logics, and
applications of those ideas.