Specifying Crash Safety for Storage Systems. - Haogang Chen 001; Daniel Ziegler 002; Adam Chlipala; M. Frans Kaashoek; Eddie Kohler; Nickolai Zeldovich (HotOS, 2015)

Using Crash Hoare Logic for Certifying the FSCQ File System. - Haogang Chen 001; Daniel Ziegler 002; Tej Chajed; Adam Chlipala; M. Frans Kaashoek; Nickolai Zeldovich (USENIX ATC, 2016)

Certifying a file system using crash hoare logic: correctness in the presence of crashes. - Tej Chajed; Haogang Chen 001; Adam Chlipala; M. Frans Kaashoek; Nickolai Zeldovich; Daniel Ziegler 002 (Commun. ACM, 2017)

Arboral satisfaction: Recognition and LP approximation. - Erik D. Demaine; Varun Ganesan; Vladislav Kontsevoi; Qipeng Liu 001; Quanquan C. Liu; Fermi Ma; Ofir Nachum; Aaron Sidford; Erik Waingarten; Daniel Ziegler 002 (Inf. Process. Lett., 2017)