I'm now managing a team at nVidia. These pages are old.
To contact me, use david@coppit.org, since I check that account more
often.
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.
Back to CSci 420/520 Homepage.