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

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




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

Professional Experience

Columbia University

    Assistant Professor (2018 - present)

Yale University

    Research Assistant, Associate Research Scientist (2011 - 2017)

    Worked on CertiKOS, an extensible architecture for building certified OS kernels. As the key developer and author of the project, I verified a series of sequential and concurrent OS kernels in Coq with my Yale colleagues. The most realistic one is written in 6,500 lines of C and x86 assembly and runs on stock x86 multicore machines.

Tsinghua University

    Research Assistant (Spring 2011)

    Worked on verifying the preemptive scheduling and nested interrupt handling of uC/OS-II running on the PowerPC platform. I presented this work in my honors undergraduate thesis.


  • 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
    • Nomination for ACM Dissertation Award
  • Aug. 2007 to Jul. 2011, Tsinghua University, B.S. in Computer Science.
    • Rank: 4/118, GPA: 91.2/100
    • Excellent Undergraduate of Tsinghua University, top 1.9% (67 among 3543)
    • Honors Undergraduate Thesis of Tsinghua University, top 4% (5 among 118)

Selected Conference Publications

Selected Talks

Introduction to CertiKOS.
Building Fully Trustworthy OS Kernels through Formal Verification.
  • Aug. 2017, University of Washinton, WA.
  • Apr. 2017, Chicago University, IL.
  • Mar. 2017, University of Minnesota Twin Cities, MN.
  • Mar. 2017, Pennsylvania State University, PA.
  • Mar. 2017, New York University, NY.
  • Mar. 2017, Boston University, MA.
  • Feb. 2017, University of Connecticut, CT.
  • Feb. 2017, Columbia University, NY.
An Extensible Architecture for Building Certified Concurrent OS Kernels.
  • Dec. 2016, University of California, Davis, CA.
  • Dec. 2016, Columbia University, NY.
  • Nov. 2016, University of Pennsylvania, PA.
  • Nov. 2016, Princeton University, NJ.
  • Nov. 2016, OSDI, GA.
Deep Specifications and Certified Abstraction Layers.

Selected Awards

Teaching Experience

Asistant Professor at Columbia University.
  • COMS E6998 Formal Verification of System Software (Fall 2018).
  • COMS W3101 Programming Languages (Python) (Spring 2018).
Teaching Asistant at Yale University.
  • CPSC 458/558 Automatic Decision Systems (Fall 2015).
  • CPSC 422/522 Operating System Design and Implementation (Fall 2015).
  • CPSC 439/539 Software Engineering (Spring 2015 and Spring 2014).
  • CPSC 424/524 Parallel Programming Techniques (Fall 2014 and Fall 2013).
  • CPSC 439/539 Software Engineering (Spring 2015 and Spring 2014).
  • CPSC 112 Introduction to Programming Languages (Spring 2013 and Fall 2012).



515 CSB, Columbia University


(212) 939-7111

CertiKOS Layers (for fun)

Layout based on BASIC by Download Website Templates