Lab 4 options

For lab 4, we would like to give you the flexibility to explore whatever direction in formal verification you think is most interesting to you. To this end, you have the choice of several options for lab 4:

The default option is doing the replicated disk lab assignment, in the same framework as labs 1, 2, and 3.

If you want to learn more about using different verification tools, consider these choices. If you are interested in pursuing this direction, get in touch with the course staff so that we know what you are working on.

• Software Foundations has a volume on verifying C code, using the Verified Software Toolchain from Princeton (built on top of CompCert). You should do all of the exercises in this volume up to but not including Verif_strlib, Hashfun, and Verif_hash. Those last three chapters are optional.

• The Iris concurrent separation logic framework has a tutorial on using Iris to verify concurrent code, in a toy language called HeapLang. After you complete the tutorial, use Iris and HeapLang to implement, specify, and prove a (sequential) hash table with linked-list chaining in each bucket.

• The Dafny tutorial introduces you to Dafny's automated verification. After you complete the tutorial, use Dafny to implement, specify, and prove a hash table with linked-list chaining in each bucket.

The final option is to do a free-form project of your choice. This might be a good idea if you are already working on a verification-related project, or have a specific idea you want to explore. Please get in touch with course staff right away if you would like to do this, so that we can help you pin down the project direction and scope.

If you are doing anything other than the default replicated disk assignment, you can ignore the intermediate deadlines for lab 4A, 4B, and 4C. You must submit your work by the lab 4D deadline. You must also contact the course staff so that we know what option you are working on.