CSci 420/520: Final Report

Due Friday, December 2nd by 1pm.

Summary

The final writeup is a formal document that describes your project.

Writing the Report

Your writeup should contain at least the following:

• A problem statement and a high level description of how the problem was addressed and solved.
• A presentation of logical representations, definitions, theorems, theories, etc. If library information (e.g. the PVS Prelude)_ was used, give a brief discussion of the parts used. You may assume the reader knows about the tool you are using, but it is not adequate simply to include raw sources. Much of your grade will depend on how you present the ideas you are using and the work you have done. For example, a common problem is to present a formal specification without explaining why certain decisions were made, and what the potential alternatives are.

• Technical presentation of the solution. Explain key ideas and key theorems in a structured, orderly progression. The first goal is to explain the mathematics of the project and not simply a "status file" of mechanized proofs, or worse, proof trees.
• Insights into the use of formal methods. What were the difficulties imposed by mechanizing the reasoning? Did you learn any new techniques? If you had to do the project again, how would you streamline the effort? In what ways did a formal approach help (or hinder) you?
• Future work. How might your work be extended?

Grading

200 points total.

Email a PDF of your proposal to meghan@cs.wm.edu.