The Palm Pilot is an increasingly popular personal digital assistant. Programs to connect it to PC's are available, but they usually cannot manipulate the data on the Palm directly. The miniproject and project would provide both the low-level (on the level of the Palm Operating System and on the level of the Linux operating system) and the high-level programs to make this direct manipulation possible.
I have developed and implemented new logics for program verification which makes it easier to construct the verification of large programs from the verification of its smaller components. I already have a preliminary implementation of this logic. Although the logic has been developed, a good way of annotating programs and verifying them automatically is missing. The miniprojects and projects would develop ways of doing this.
Page maintained by E.Ritter@cs.bham.ac.uk
Last modified: Tue Sep 3 16:49:57 BST 2002