Applying Formal Methods to Operating Systems

Several of our students performed an ambitious experiment with formal methods, verifying a model of the Fluke IPC path. They found some interesting results! A paper describing their experience, several presentations, a class report, the model-- in PROMELA, and some tools (hacks) are available now.

We and external collaborators will likely continue to pursue this type of work. In addition, there is DARPA-funded research on formal methods themselves, in an allied project at Utah, led by Ganesh Gopalakrishnan.

Up to Flux project home page
Last modified on Oct 20 2000