[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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.
Applications are now being accepted <https://goo.gl/forms/M54ML7W7vtcSt3fW2>!
Overview
Can critical systems be built with zero bugs in critical components such as
hardware, operating systems, compilers, or crypto? It may seem a pipe dream,
but in fact the past decade has seen explosive 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 complete the summer school with 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.
Dates
The summer school will open with a three-day intensive course on Coq
fundamentals, 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
Prerequisites
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 <https://www.cis.upenn.edu/~bcpierce/sf/current/index.html> should
plan on attending the Coq Intensive before the summer school.
Costs and Financial Aid
The total cost (for lectures, meals, and dormitory lodging) is expected to be
roughly $2000 per participant.
Substantial subsidies are available, courtesy of the NSF (thank you!), for
students requiring financial assistance to attend. More details will be
announced when applications open.
Applications
Applications are now open (here) <https://goo.gl/forms/M54ML7W7vtcSt3fW2>!
Applications received by Feb 15 will be given equal consideration; applications
received after Feb 15 will be considered on a space-available basis.
