Overview

Based on what you learn in this class, you will be expected to complete a research project in the space of verifying complex systems. The typical form of the project will be to specify and implement a system using verification tools such as Z3, Rosette, Dafny, F*, Lean, or Coq, and then formally verify that the implementation meets the specification. Many variations on this theme are possible. If your usual research is not on verification, then you are encouraged to consider intersections between your research and the topics in this class. If your usual research is already in the space of verification, I would encourage you to find an aspect unique to this class, or even to experiment with something new that you don’t typically use. You will get much more out of this class and the project if you use it as an opportunity to explore beyond your typical tools and techniques.

You may work in groups of 1-3 students (total), but my expectations for the project will grow superlinearly (but subquadratically) with group size.

You’ll turn in your code and a paper describing the design and implementation, which we will post on the course website (unless you explicitly talk to us about why you want to keep it confidential). Use the OSDI’16 submission format for your paper.

Overall, you will be expected to submit a one-page project proposal (10% of your project grade), a mid-point checkpoint report (20%), and then a final report (40%) and presentation to the class (30%). The checkpoint report should be a 5-6 page PDF describing your progress achieving your initial goals. It should clearly explain any changes you have made to the goal of your project based on your experience so far. Include examples that your prototype can already handle. Provide a clear, concrete plan of what you will need to accomplish in the remaining weeks to complete your project and what we can expect to see in the presentation. The report should also include a high-level literature review of papers (both from inside and outside of class) most relevant to your project. The final report should be on the order of 10-12 pages, written in the style of the research papers we’ve read in class.
It should describe your system and evaluate using the metrics we’ve applied to each system we’ve read about. Please be clear on what your system does and does not guarantee, as well as opportunities for extending and improving on your work.

Here’s a list of ideas to get you started. Feel free to pursue your own ideas or to discuss early ideas with me.

Schedule

Please see the calendar for project-related due dates.

Project ideas

Here is a list of ideas to get you started thinking. Feel free to pursue your own ideas.