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.
I am also a co-founder of CertiK, a formal verification startup based on my research.
Hiring!
-
My research group at Columbia University is looking for Ph.D./Master students, Postdocs, and Undergraduate interns.
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 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.
Education
- 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
-
[PLDI 2018] Certified Concurrent Abstraction Layers.
(with Z. Shao, J. Kim, X. Wu, J. Koenig, V. Sjoberg, C. Hao, D. Constanzo, and T.Ramananandro)
-
[OOPSLA 2017] An Auditing Language for Preventing Correlated Failures in the Cloud.
(with with Ennan Zhai, Ruzica Piskac, Xun Lao, and Xi Wang)
-
[OSDI 2016] CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels.
(with Z. Shao, C. Hao, X. Wu, J. Kim, V. Sjoberg, and D. Constanzo)
Media coverage: Yale News, International Business Times, Yale Daily News
Honor: Selected in the Research Highlights section of the CACM.
-
[PLDI 2016] End-to-End Verification of Information-Flow Security for C and Assembly Programs.
(with D. Constanzo and Z. Shao)
-
[PLDI 2016] Toward Compositional Verification of Interruptible OS Kernels and Device Drivers.
[POPL 2015] Deep specifications and Certified Abstraction Layers.
(with J. Koenig, T. Ramananandro, Z. Shao, X. Wu, S. Weng, H. Zhang, and Y. Guo)
Professional Activities
- PC: NSDI'19, CoqPL'19, SecDev'18, ICFP'18 SRC.
- ERC: PLDI'18.
Teaching
- COMS E6998 Formal Verification of System Software (Fall 2018).
- COMS W3101 Programming Languages (Python) (Spring 2018).
Selected Awards
- Dec. 2016, Distinction Dissertation, Yale University.
- Aug. 2016, Nomination for ACM Dissertation Award, Yale University.
- Feb. 2016, Robert Willets Carle Scholarship, Yale University.
- Jul. 2011, Excellent Undergraduate (top 1.9%), Tsinghua University.
- Jul. 2011, Excellent Undergraduate of Beijing City, China.
- Jul. 2011, Hornors Undergraduate Thesis Award, 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.
Office
515 CSB, Columbia University
Phone
+1 (212) 939-7111
CertiKOS Layers (for fun)
