Paper on formal specificaiton and testing of filesystems at SOSP 2015
SibylFS: formal specification and oracle-based testing for POSIX and real-world file systemsTom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, and Peter Sewell.Paper in the proceedings of the 25th Symposium on Operating Systems Principles.URL (dl.acm.org) DOI BIB PDF
SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems
Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, and Peter Sewell.
Paper in the proceedings of the 25th Symposium on Operating Systems Principles.
URL (dl.acm.org) DOI BIB PDF
Anil Madhavapeddy, Professor of Planetary Computing 
papers