CS195y Final Project

The final project for this course is to rigorously model a topic of interest to you and a partner. Project topics can be anything substantial that touches on modeling and verifying software or systems. You can think of your topic as selecting a problem and modeling it in the interest of something we should care about. For example, your topic could be modeling a specific algorithm in Alloy in the interest of verifying the various runtime or correctness properties the algorithm is expected to have.

Prior successful topics have included data-structures, communication protocols, user-interfaces, games, and more. Alloy is well-suited for most final projects. However, if your topic requires multi-processors, true mathematical integers, or something else that Alloy does not handle gracefully, you may also use Z3 or Spin (or another tool with instructor permission).

Proposal

Project proposals are due on April 7th via email to Tim, and must be discussed with the course staff at office hours prior to approval. The proposal should be no more than one page, and should include:

• A description of the topic, i.e., what the problem you intend to model is
• Why the topic is interesting
• Three benchmark goals for your project:
  1. A foundation goal. This should be the basic functionality you plan on completing, the component(s) and property verification(s) you are confident that you will be able to accomplish.
  2. A target goal. This should describe the project you plan on handing in, and should include some interesting component(s) and property verification(s) that you would are fairly sure you will be able to complete.
  3. A reach goal. This should be something extra that you may attempt after you complete the rest of your project. It can be something that you aren’t sure is possible!

Final Submission

Projects (the source code along with a one page writeup/README) are due electronically on May 9th. Each group will then present their final project to Tim, in a format similar to the case-study reviews, by appointment during May 10th–12th.