Describir: Certifying a File System Using Crash Hoare Logic: Correctness in the Presence of Crashes.