Using Crash Hoare logic for certifying the FSCQ file system.

Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich

Browse the full SOSP paper archive.