Generated on 20170305 | Print

Yuan, Xinhao


1214 Amsterdam Ave
450 Computer Science Building
New York, NY 10027


  • 2012-presentMS/PhD, Columbia University
    Department of Computer Science
  • 2007-2011B.Eng, Tsinghua University
    Department of Computer Science and Technology


  • Strong background in math, algorithms, programming, and software systems
  • Fast learner who can master new technology quickly
  • Passionate for creative software system research

- basic,
- experienced,
- expert


Operating System
Distributed System
Formal Methods




  • Libraries/Frameworks:
    Android, LLVM, jQuery/LESSCSS
  • Strong hands-on experience with GNU/Linux environment

Working Experience

  • 2012-presentResearch Assistant, Columbia University, Advisor: Junfeng Yang
    • Working on research projects of model checking and other formal methods for reliability of software systems
  • 2016/01-2016/05Intern as Contractor, Microsoft/Microsoft Research, Mentor: Cheng Huang
    • Worked on applying model checking method on Azure Storage system to improve its reliability
  • 2015/06-2015/08Research Intern, Microsoft Research, Mentor: Lidong Zhou
    • Worked on distributed computing platform specialized for social analytics
    • Extended Naiad dataflow system to support consistent dataflow mutation on the fly
  • 2009-2011Research Intern at System Research Group, Microsoft Research Asia, Mentor: Ming Wu
    • Implemented the TPC-C benchmark for Hyder project and published paper [2] in VLDB 2011.
    • Awarded "Stars of Tomorrow" internship certificate for the excellent performance

Projects More hosted on

  • DrillMC, a practical model checking framework for distributed software systems
  • Txit [1], a framework to make lock-free data structures managable to verify by leveraging transactional memory
  • AppDoctor [2], a model checker that systematically tests user interactions of android apps to find crash bugs
    • Built the instrumenter that interposes the android framework to control the I/O and event handling of apps
  • Hyder [3], a transactional key-value database system backed by shared log storage with a novel concurrency control protocol
    • Worked with my mentor to implement and refine the prototype system
    • Implemented the TPC-C benchmark on the prototype


[1]Make Lock-free Data Structures Verifiable with Artificial Transactions. PLOS 2015. Xinhao Yuan, David Williams-King, Junfeng Yang, Simha Sethumadhavan
[2]Efficiently, effectively detecting mobile app bugs with AppDoctor. In Proceedings of the Ninth European Conference on Computer Systems (EuroSys '14). Gang Hu, Xinhao Yuan, Yang Tang, Junfeng Yang
[3]Optimistic Concurrency Control by Melding Trees, VLDB 2011. Phil Bernstein, Colin Reid, Ming Wu, Xinhao Yuan
[4]S-FTL: An Efficient Address Translation for Flash Memory by Exploiting Spatial Locality, MSST 2011. Song Jiang, Lei Zhang, Xinhao Yuan, Hao Hu, Yu Chen


  • 27th place in 37th Annual World Finals of the ACM International Collegiate Programming Contest (2013)
  • Champion of ACM/ICPC '12, Greater New York Region
  • Gold medal in the National Olympiad in Informatics '06, China