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 USENIX paper archive.