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.

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.