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.


My research group at Columbia University is looking for Ph.D./Master students, and Postdocs. Check out our recent CACM Research Highlights, 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, 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