DeepSpec Summer School 2017 - a summary
I have spent the last two and a half week in Philadelphia attending the first DeepSpec Summer School, In this post I want to summarize the event and give an overview of all the courses.
The DeepSpec Project is a research project lead by several US East Coast universities (University of Pennsylvania, MIT, Yale University and Princeton University) and aims to “push forward the state of the art in applying computer proof assistants to verify realistic software and hardware stacks at scale”. It consists of several smaller projects, including a formal verification of a hypervisor (CertiKOS), LLVM (Vellvm), Coq compiler (CertiCoq) and GHC’s Core language (CoreSpec).
The goal of DeepSpec Summer School was to introduce people to real-life formal verification using Coq proof assistant. School was divided into three parts. All the lectures can be found on a YouTube channel. Coq code for the courses is available on GitHub. Summer school’s web page also provides installation instructions as well as other supplementary material (click on a given lecture or select from “Lectures” tab).
Week 0: Coq Intensive
First three days of the summer school were a very intensive introductory course on Coq lead by Benjamin Pierce. This essentially covered the first volume of Software Foundations. (Aside: For those of you who don’t know yet, original Software Foundations online book has been split into two volumes: Logical Foundations and Programming Language Foundations. Also, a third volume has been added to the series: Verified Functional Algorithms by Andrew Appel. All three volumes can be found here, although expect that this link will likely become broken soon when this draft versions become an official release. There are also plans for two more volumes, one on Separation Logic and another one on Systems Verification.)
Week 1: Programming Language Verification
First full week of the school consisted of four courses centred around programming language verification:
Property-based random testing with QuickChick by Benjamin Pierce. I assume many of you heard about Haskell library called QuickCheck. It offers property-based testing: programmer writes properties that the should hold for a given piece of code and QuickCheck tests whether they hold for randomly generated test data. QuickChick is implementation of the same idea in Coq. Now, you might wonder what is the point of doing such a thing in Coq. After all, Coq is about formally proving that a given property is always true, not randomly testing whether it holds. I was sceptical about this as well, but it actually turns to be quite a good idea. The point is, specifications are difficult to write and often even more difficult to prove. They are especially difficult to prove when they are false ;-) And this is exactly when QuickChick can be beneficial: by trying to find a counter-example for which a stated property does not hold. This can indeed save programmer from spending hours on trying to prove something that is false. If QuickChick doesn’t find a counter-example we can start writing a formal proof. This course also gives a nice overview of type classes in Coq.
The structure of verified compiler by Xavier Leroy. This series of lectures was based on CompCert, which is a formally verified C compiler. The ideas behind formal verification of a compiler were presented on a compiler of Imp (a toy imperative language used in Software Foundations) to a simple virtual machine. Fourth, final lecture covered the CompCert project itself. To me this was the most interesting course of the summer school.
Language specification and variable binding by Stephanie Weirich. Software Foundations is a great book, but it completely omits one topic that is very important in formalizing programming languages: dealing with variable bindings. In this courses Stephanie presented “locally nameless” representation of variable bindings. This is something I had planned to learn for a very long time but couldn’t find the time.
Vellvm: Verifying the LLVM by Steve Zdancewic. For a change, in this course Imp was compiled to a simplified variant of LLVM, the compilation process being verified of course. Also, a nice introduction to LLVM.
Week 2: Systems Verification
Courses during the second week put more focus on verifying computer systems. Again, there were four courses:
Certifying software with crashes by Frans Kaashoek and Nickolai Zeldovich. The topic of this course was certification of a hard-drive operating routines, including bad-sector remapping and a simple virtual RAID 1 implementation. Although still using toy examples, specifications presented during this course were much more abstract giving a good idea how to scale to a real-world system verification. I found this course very difficult to follow, although the lectures were really superb. Note: materials for this one course are available in a separate GitHub repo.
CertiKOS: Certified kit operating systems by Zhong Shao. Ok, I admit I was completely unable to follow this series of lectures. Way to difficult. In fact, I skipped two out of four lectures because I figured out it will make more sense to work on homework assignments for other lectures.
Program-specific proof automation by Adam Chlipala. Unsurprisingly to those who know Adam’s “Certified Programming with Dependent Types” book, his course focused on proof automation using Ltac. One lecture was specifically dedicated to proofs by reflection.
Verified Functional Algorithms by Andrew Appel. This course covered a majority of third volume of new Software Foundations.
Summary
First and foremost let me say this: DeepSpec Summer School was the best research meeting I have ever attended. The courses were really good and inspiring, but the most important thing that made this summer school so great were fantastic people who attended it. Spending evening hours together working on homework assignments was especially enjoyable.
There might be a 2018 edition of the summer school so be on the lookout - this is a really great event for anyone interested in Coq and formal verification.