The second DeepSpec Summer School on Verified Systems will be held in Princeton, NJ from July 16 to 27, 2018, including an introductory Coq Intensive from July 16 to 18. 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'18 will consist of two parts with the first week being devoted to introductory topics and the second week covering current research efforts.

July 16-18 (Mon-Wed)	Coq intensive
July 19-20 (Thu-Fri)	Fundamental proof techniques and project overviews
July 23-27 (week 2)	Advanced topics in system verification

Lecturers and Topics for week 2

Andrew Appel & Lennart Beringer	Verifiable C: a logic and toolset for proving C programs correct
Adam Chlipala	Implementing, specifying, verifying, and compiling hardware components with Kami
Zach Tatlock	Verifying distributed systems
Benjamin Pierce	Property-based random testing with QuickChick
All DeepSpec PIs	Towards the specification and verification of a web server

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 are likely to be admitted for participation in week 2 only.

Application and participation

Participation in DSSS'18 is by invitation only, based on an application process that is open to anybody. The application deadline has now passed.

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 will offer free dorm accommodation on the campus of Princeton University. In addition, we expect to subsidize travel expenses for the majority of participants, based on their geographic origin, qualification, and financial needs. To help us allocating 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.

---