|CSCI P545||Fri Jan 6 15:18:04 EST 2012 [SDJ]|
Your score will be scaled in proportion to the problem's degree of difficulty.
In some cases, the problem is only briefly described, without much guidance about how to approach it. Consult with the instructor about how to get started with a problem.
If you just want to be done with this course, I have a set of old homework assignments. You can as many as you can, but this option is unlikely to yield an A in P415/P515.
The MergeSort and QuickSort list-sorting algoritms are formulated in PVS. The problem is to prove them correct, similar to BubbleSort and InsertionSort algorithms in Homework Assignment 7.
Model and verify an in-place, array-reversal program.
Model and verify an in-place, array-sorting program.
Since the problem is intended to illustrate the interplay of design assumptions and requirements specification, it is better for a team of at least two people to work independently on the problem and then "cross verify" the pieces in various combinations.
The Dining Philosophers Problem, due to Dijkstra, is standard in most Operating Systems Textbooks for illustrating weaker forms of mutual exclusion. Specifically, it is a metaphore for concurrent systems in which each process requires exclusive access to multiple conflicting resources. How to solve the problem depends on atomicity assumptions, and it is easy to oversimplify.