Towards Certified Storage Systems

Haogang Chen, Daniel Ziegler, Adam Chlipala, Frans Kaashoek, Eddie Kohler, Nickolai Zeldovich. Towards Certified Storage Systems. Proceedings of the 15th Workshop on Hot Topics in Operating Systems (HotOS'15). May 2015.

Paper as PDF

On verifying functional properties of filesystems in the presence of failures, using proof assistants