The Science of Deep Specification
Incomplete group photo

The first DeepSpec Summer School on Verified Systems was be held in Philadelphia from July 17 to 28, 2017, preceded by an introductory Coq Intensive from July 13 to 15.


Can critical systems be built with no bugs in hardware, operating systems, compilers, crypto, or other key components? It may seem a pipe dream, but the past decade has seen remarkable advances in the technology required to realize it.


The Summer School is supported by generous contributions from


The summer school will open with a three-day intensive course on the fundamentals of the Coq proof assistant, for participants who are new to Coq. The main lectures take place during the weeks of July 17 and 24.

July 13-15 (Thu-Sat) Coq intensive
July 17-21 Week 1
July 24-28 Week 2

Lecturers and Topics

Andrew Appel Verified functional algorithms
Adam Chlipala Program-specific proof automation
Frans Kaashoek & Nickolai Zeldovich Certifying software with crashes
Xavier Leroy The structure of a verified compiler
Benjamin Pierce Property-based random testing with QuickChick
Zhong Shao CertiKOS: Certified kit operating systems
Stephanie Weirich Language specification and variable binding
Steve Zdancewic Vellvm: Verifying the LLVM


The DeepSpec summer school is aimed at a wide range of participants, including graduate students, academics, and industrial engineers and researchers.

The Coq proof assistant will serve as a lingua franca for all the lectures. Participants who are not already familiar with Coq at the level of Software Foundations should plan on attending the Coq Intensive before the summer school.


Questions about the summer school should be directed to Benjamin Pierce.