Verifying a high-performance crash-safe file system using a tree specification. - Haogang Chen 001; Tej Chajed; Alex Konradi; Stephanie Wang; Atalay Mert Ileri; Adam Chlipala; M. Frans Kaashoek; Nickolai Zeldovich (SOSP, 2017)