The first DeepSpec Summer School on Verified Systems will be held in Philadelphia from July 17 to 28, 2017, preceded by an introductory Coq Intensive from July 13 to 15.
are closed for the summer school. However,
additional spaces may be available for the Coq intensive and the first
week (only) of the school, for self-funding participants. If you are
interested in attending for one or both of these, please add your name to
the DeepSpec mailing list; we will post a message there
when registration re-opens.
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.
This summer school aims to give participants a wide-ranging overview of several ambitious projects currently underway in this space. Participants will gain a thorough understanding of the conceptual underpinnings of these projects plus considerable hands-on experience with state-of-the-art tools for building verified systems
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|
|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.
Substantial subsidies are available, courtesy of the NSF (thank you!), for students requiring financial assistance to attend.