CSCI P545 Fri Jan 6 15:18:04 EST 2012 [SDJ]

### P415/P515 Projects

Do one of the following assignments:
• 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.

#### PVS projects

1. Get-me-outta-here [3–5]

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.

2. Recursive List Sorts [6]

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.

3. Array Reversal [7]

Model and verify an in-place, array-reversal program.

4. Array Sorting [9]

Model and verify an in-place, array-sorting program.

5. Search Structures [7–9]

#### SMV problems

I don't recommend doing an SVM problem for this assignment, but I am willing to discuss it with anyone who is really interested in learning more about model checking.

1. Island Tunnel Controller [3–5] The Island Tunnel Controller is a variation on the simple traffic light controller. It has also been compared to the Clayton Tunnel protocol. A module for traffic-light control for a one-lane tunnel is the first half of the problem. The second half is to write a module representing constraints on the behavior of the environment (the cars), and model-check the composition of these two modules.

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.

2. Dining Philosophers [4–6]

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.

3. Elevator Problem [4–6] The project is to model the Lindley Hall elevator and verify liveness properties for different control strategies. I have not written this project specification yet, but if you wish to explore it, let me know.