The third DeepSpec Summer School on Verified Systems will be held in New Haven, CT from July 13 to 24, 2020, including an introductory Coq Intensive from July 13 to 15. The Summer School is supported by generous funding from the National Science Foundation (under grant #1521523, Expeditions in Computing: The Science of Deep Specification).

Overview

Can critical systems be built according to functionally precise specifications of of their constituent components (processor, operating system, crypto library,..) and development tools (compilers, synthesis tools)? This may seem a pipe dream, but the past decade has seen remarkable advances in the technology required to realize it. The DeepSpec Summer School will provide students with knowledge and experience necessary for understanding the state of the art and for contributing to ongoing research efforts, based on the interactive proof assistant Coq. DSSS'20 will consist of two parts, with the first week being devoted to introductory topics and the second week covering current research efforts.

July 13-15 (Mon-Wed)	Coq intensive; CertiKOS design & spec	Appel, Pierce, Zdancewic; Shao
July 16-17 (Thu-Fri)	Fundamental proof techniques and project overviews	Appel, Tassarotti
July 20-24 (week 2)	Advanced topics in system verification	Chlipala, Pierce, Shao, Sozeau, Weirich, Zdancewic

Lecturers and Topics

End of Week 1	Andrew Appel	Verified Functional Algorithms
	Joseph Tassarotti	TBD (on Iris)
Week 2	Adam Chlipala	Connecting Hardware & Software Proofs
	Benjamin Pierce	Property-Based Testing in Coq
	Zhong Shao	From Hacker-Resistant OS to Certified Heterogeneous Systems
	Matthieu Sozeau	The MetaCoq Framework: Metaprogramming and Metatheory of Coq in Coq; The Coq Project and Platform
	Stephanie Weirich	Verifying Functional Algorithms with hs-to-coq
	Steve Zdancewic	Interaction Trees and Compositional Compiler Correctness

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 familiar with Coq at the level of Software Foundations (Volume 1) should plan on attending the Coq Intensive. Participants unfamiliar with volumes 2 and 3 may benefit from attending the last 3 days of week 1.

Participants of DSSS'17 and DSSS'18 are likely to be admitted for participation in week 2 only.

Application and participation

Participation in DSSS'20 is by invitation only, based on an application process that is open to anybody. To apply, please submit the application form, preferably no later than March 27, 2020. Accepted participants will be notified shortly thereafter, and will be invited to confirm their participation by registering.

Thanks to the generosity of NSF, we will be able to provide substantial financial assistance to all participants. We will not charge a registration fee, and we will offer free dorm accommodation on the campus of Yale University. In addition, we expect to subsidize travel expenses for the majority of participants, based on their geographic origins, qualifications, and financial needs. To help us allocate these funds, the application form includes the option to enter estimated travel costs, etc.

Late applications will be handled on a case-by-case basis.

Questions

Questions about the summer school should be directed to Lennart Beringer.

---