Gabriele Keller
University of New South Wales

File System Verification

File systems are too important, and current ones are too buggy, to remain
unverified. Yet the most successful verification methods for functional
correctness remain too expensive for current file system implementations — we
need verified correctness but at  reasonable cost. In this talk, I present a
implementation & verification framework, which aims at reducing the costs of
developing  fully verified file systems significantly. It is based on a
careful, modular design to maximise reusability of components shared across
different systems  to reduce the cost of high level verification, and the use
of two domain specific languages with strong type systems to generate both
code and low level correctness proofs.