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.
    • Advisor: Professor Zhong Shao
    • Thesis: An Extensible Architecture for Building Certified Sequential and Concurrent OS Kernels.
    • 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, 3 among 140


Select Publications

Program Committees

    PLDI 2020 SecDev 2020 NSDI 2019 SoCC 2019
    SecDev 2019 PLDI 2018 ERC SecDev 2018 ICFP 2018 SRC


I am fortunate to work or have worked with these brilliant students.

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
    Columbia-IBM Center Seed Grant Award Dec. 2018
    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 (3 among 140), Tsinghua University July 2011
    Outstanding Undergraduate of Beijing City, China July 2011
    Honors Undergraduate Thesis Award (5 among 140), Tsinghua University July 2011
    First Prize of National Mathematical Olympiad Competition, China Oct. 2006



515 CSB, Columbia University


+1 (212) 939-7111

CertiKOS Video (for CACM)

CertiKOS Layers (for fun)

Layout based on BASIC by Download Website Templates