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
Certifying software with crashes
Frans Kaashoek & Nickolai Zeldovich
Lecture recordings
Video 1
Video 2
Video 3
Video 4
