Provably Correct Software, Spring -10

A selection of previous student projects

Code lock system
Web store
Bus service database
Calculator
Balanced binary search trees (the mathematical reasoning about the balancing condition was very difficult)
Student data base
Tic-tac-toe
Text formatter (the specification was difficult to get right)

Some project suggestions

Online reservation system with multiple clients