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 am also a co-founder of CertiK, a formal verification startup. Press on CertiK: Forbes, Coindesk, Yale News.

[CV.pdf] [ResearchStatement.pdf]


My research group at Columbia University is looking for Ph.D./Master students, and Postdocs. Check out our recent PLDI'18, OSDI'16, and POPL'15 CertiKOS papers (and the press release) for an overview of our latest breakthrough on building bug-free and hacker-resistant OS kernels. If you know both systems and programming languages, and are interested in building certified systems, send me an email.


Selected Publications

Program Committee

    PLDI'20, NSDI'19, SoCC'19, SecDev'19, CoqPL'19, PLDI'18 ERC, SecDev'18 ICFP'18 SRC.

Selected Awards

  • Feb. 2019, MIT Technology Review 35 Innovators Under 35 Semi-Finalist.
  • Dec. 2016, Distinction Dissertation, Yale University.
  • Aug. 2016, Yale Nominee, ACM Doctoral Dissertation Award.
  • Feb. 2016, Robert Willets Carle Scholarship, Yale University.
  • Aug. 2011, Doctoral Fellowship, Yale University.
  • Jul. 2011, Outstanding Undergraduate (67 among 3540), Tsinghua University.
  • Jul. 2011, Outstanding Student of Beijing City, China.
  • Jul. 2011, Hornors Undergraduate Thesis Award (5 among 140), Tsinghua University.
  • Oct. 2010, Sohu Scholarship, Tsinghua University.
  • Oct. 2009, Ticket Master Scholarship, Tsinghua University.
  • Oct. 2006, First Prize of National Mathematical Olympiad Competition, China.



515 CSB, Columbia University


+1 (212) 939-7111

CertiKOS Layers (for fun)

Layout based on BASIC by Download Website Templates