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