Linux kernel vulnerabilities: state-of-the-art defenses and open problems. - Haogang Chen 001; Yandong Mao; Xi Wang 005; Dong Zhou 006; Nickolai Zeldovich; M. Frans Kaashoek (APSys, 2011)

Software fault isolation with API integrity and multi-principal modules. - Yandong Mao; Haogang Chen 001; Dong Zhou 006; Xi Wang 005; Nickolai Zeldovich; M. Frans Kaashoek (SOSP, 2011)

Undefined behavior: what happened to my code? - Xi Wang 005; Haogang Chen 001; Alvin Cheung; Zhihao Jia; Nickolai Zeldovich; M. Frans Kaashoek (APSys, 2012)

Improving Integer Security for Systems with KINT. - Xi Wang 005; Haogang Chen 001; Zhihao Jia; Nickolai Zeldovich; M. Frans Kaashoek (OSDI, 2012)

Security bugs in embedded interpreters. - Haogang Chen 001; Cody Cutler; Taesoo Kim; Yandong Mao; Xi Wang 005; Nickolai Zeldovich; M. Frans Kaashoek (APSys, 2013)

Why does cryptographic software fail?: a case study and open problems. - David Lazar; Haogang Chen 001; Xi Wang 005; Nickolai Zeldovich (APSys, 2014)

Identifying Information Disclosure in Web Applications with Retroactive Auditing. - Haogang Chen 001; Taesoo Kim; Xi Wang 005; Nickolai Zeldovich; M. Frans Kaashoek (OSDI, 2014)

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 crash-safe file system. - Haogang Chen 001 (2016)

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)

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)