SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems / Oct 2015
Paper on formal specification and testing of filesystems at SOSP 2015, the premier operating systems conference. SibylFS with Tom Ridge, David Sheets, Peter Sewell and colleagues created the first comprehensive formal specification of POSIX filesystem behavior, then used it as a test oracle to discover numerous inconsistencies and bugs in real-world filesystems. The work demonstrated how executable specifications could bridge theory and practice, finding genuine bugs in production Linux and BSD filesystem implementations that had existed for years.