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 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

  • Oct. 2019, SOSP Best Paper Award.
  • Oct. 2019, Communications of the ACM (CACM) Research Highlights.
  • Feb. 2019, MIT Technology Review 35 Innovators Under 35 Semi-Finalist.
  • Dec. 2018, Columbia-IBM Center Seed Grant Award.
  • Dec. 2016, Distinction Dissertation, Yale University.
  • Aug. 2016, Yale Nominee, ACM Doctoral Dissertation Award.
  • Feb. 2016, Robert Willets Carle Scholarship, Yale University.
  • Jul. 2011, Graduation with Highest Distinction (3 among 140), Tsinghua University.
  • Jul. 2011, Outstanding Student of Beijing City, China.
  • Jul. 2011, Hornors Undergraduate Thesis Award (5 among 140), Tsinghua University.
  • Oct. 2006, First Prize of National Mathematical Olympiad Competition, China.



515 CSB, Columbia University


+1 (212) 939-7111

CertiKOS Video (for CACM)

CertiKOS Layers (for fun)

Layout based on BASIC by Download Website Templates