I am an Assistant Professor of Computer Science at Columbia University.

My research interests span a range of areas in Programming Languages, Operating Systems, and Blockchain Systems, with a focus on language-based support for safety and security, certified system software, certified programming and compilation, formal methods, and concurrency reasoning.

I co-founded CertiK, a systems verification startup. Press on CertiK: Forbes, Coindesk, Yale News.


My research group at Columbia University is looking for Ph.D./Master students, and Postdocs. Check out our recent CACM Research Highlights, SOSP'19 (Best Paper Award), PLDI'18, OSDI'16, and POPL'15 papers (and the press release) for an overview of our latest breakthrough on building bug-free and hacker-resistant systems software.


  • Aug. 2011 to Aug. 2016, Yale University, Ph.D. in Computer Science.
    • Distinction Dissertation of Yale Graduate School of Art and Science
    • Yale Nominee of the ACM Doctoral Dissertation Award
  • Aug. 2007 to Jul. 2011, Tsinghua University, B.S. in Computer Science.
    • Rank: 4/140, Graduation with Highest Distinction (top 1.9%)


Select Publications

Select Awards

    Columbia University’s Final Nominee for the Packard Fellowship Mar. 2020
    SOSP Best Paper Award Oct. 2019
    Communications of the ACM (CACM) Research Highlights Oct. 2019
    MIT Technology Review 35 Innovators Under 35 Semi-Finalist Feb. 2019
    Distinction Dissertation, Yale University Dec. 2016
    Yale Nominee, ACM Doctoral Dissertation Award Aug. 2016
    Robert Willets Carle Scholarship, Yale University Feb. 2016
    Graduation with Highest Distinction (top 1.9%), Tsinghua University July 2011
    Outstanding Undergraduate of Beijing City, China July 2011
    Honors Undergraduate Thesis Award (5 among 140), Tsinghua University July 2011

Program Committees

    OSDI 2021 PLDI 2020 SecDev 2020 NSDI 2019 SoCC 2019
    CoqPL 2019 SecDev 2019 PLDI 2018 ERC SecDev 2018 ICFP 2018 SRC




515 CSB, Columbia University


+1 (212) 939-7111

CertiKOS Video (for CACM)

CertiKOS Layers (for fun)

Layout based on BASIC by Download Website Templates