Toggle navigation
Summer School
Logistics
Installation
Schedule
Lectures
Coq Intensive
Verified functional algorithms
Program-specific proof automation
Certifying software with crashes
The structure of a verified compiler
Property-based random testing with QuickChick
CertiKOS: Certified kit operating systems
Language specification and variable binding
Vellvm: Verifying the LLVM
YouTube channel
DeepSpec Summer School, July 13-28, 2017
Vellvm: Verifying the LLVM
Steve Zdancewic
Lecture 1: Introduction to LLVM & Vminus
Material
slides
Lecture recordings
Video 1
Lecture 2: Operational Semantics & Dominators
Material
slides
Lecture recordings
Video 2
Lecture 3: Imp to Vminus
Material
See the Coq developments.
Lecture recordings
Video 3
Lecture 4: SSA Optimizations and Scaling Up
Material
slides
Lecture recordings
Video 4
