DeepSpec Summer School, July 16-27, 2018: schedule
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) |
|
|||
| July 19-20 |
|
The lectures in the second week (July 23-27) will cover advanced topics in-depth.
- Property-based random testing with QuickChick (Pierce, Lampropoulos)
- Correct Hardware synthesis using Kami (Chlipala)
- Verifiable C and the Verified Software Toolchain (Appel, Beringer)
- Verification of Distributed Systems using Verdi (Tatlock)
- Towards a verified Web server (Pierce, Beringer)
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.