The Science of Deep Specification

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. Concurrently, Coq-proficient users may participate in a VST hackathon -- lighty advised verification of C programs using VST.

The lectures on July 19 and July 20 will present general techniques on writing and verifying programs in Coq, together with overview presentations on Narcissus and CertiKOS.

July 16-18 (Mon-Wed)
Coq intensive (Pierce, Delaware, Beringer, Appel)
or: Verifiable C hackathon, for experienced Coq users
July 19-20
Verified functional algorithms; proof automation (Appel)
and: Overwiew Narcissus (Delaware)
and: Overview CertiKOS (Gu, Shao)

The lectures in the second week (July 23-27) will cover advanced topics in-depth.

Lectures start generally at 9am, preceded by on-site light breakfast. Lecture days will have two 90-minute lectures in the morning, followed by lunch and a 2h homework session which participants may use to work - individually or in small groups - through the Coq developments associated with the lectures or solve exercises that may be set by the lecturers. Afternoon coffee will be followed by a third 90-minute lecture.

On one of the last days, a representative from the Coq team will be present, to collect feedback and give an update on ongoing and future developments.

The last lecture will end by 4PM on July 27th; dorm rooms are available for one additional night.

A preliminary second-week schedule is as follows

Mon, July 23 QuickChick + Kami + QuickChick
Tue, July 24 QuickChick + Kami + VST
Wed, July 25 Verdi + Kami + Webserver/Testing
Thu, July 26 VST + Verdi + CoqTeam
Fri, July 27 VST + Verdi + Webserver/VST

Preparation: installation and self-study

Participants should bring their own laptop and have Coq 8.8 installed, with CoqIDE or Proof General. In case you experience problems, please make use of the Slack channel or contact the organizers.

Participants in the Coq Intensive course in week 1 should additionally download at least Volume 1: Logical Foundations of Software Foundations, read carefully through the first four chapters (Preface, Basics, Induction, and Lists), and complete all the exercises marked required in these chapters. This should take on the order of 10-20 hours of work. The summer school lectures will begin with a brief discussion of these chapters, mainly to answer questions, and then proceed more slowly beginning with chapter Poly. Feel free to use the Slack channel to discuss any questions that arise.

Participants in the VST hackathon should install Version 2.2 of the Verified Software Toolchain (alternatively, the master branch from github should also be ok), make sure that "make" succeeds, and skim the first eight chapters of the manual. Again, feel free to use the Slack channel to discuss any questions that arise.

Participants in Verified functional algorithms and proof automation should install volumes 1 and 3 of Software Foundations and (if necessary) brush up on programming in a strongly typed functional language such as ML/OCaml or Haskell.

A github repository for additional Coq material associated with lectures in week 2 will be made available shortly before the summer school.

Optional activities

Student-organized additional sessions will be coordinated by Roberto Blanco and Calvin Beck and may include ad-hoc topical Coq-formalization efforts, presentations of ongoing research, or other activities.

For information concerning the beach excursion and local attractions please see the "Logistics" tab.