Xiaohong Chen 陈霄泓

Welcome to my homepage. I'm a PhD student in Computer Science at University of Illinois Urbana-Champaign. My research interests are in logic, formal methods, and programming languages.

I’m applying for a tenure-track faculty position.

Find my application below:

My currenct research topics include:

  • matching logic [link]: a unifying logic foundation for programming languages, program properties, and program analysis, with a powerful proof system and a small proof checker. I study matching logic’s expressive power, soundness and completeness properties, decision procedures, and tool support for both interactive and automated reasoning.
  • K framework [link]: a unifying semantics-based language framework, with a set of high-performance semantics-based language tools.
  • proof generation: a practical technique to provide formal correctness guarantees to semantics-based language implementations and formal analysis tools. Computation and formal verification are certified by complete, rigorous, transparent, human-accessible, and machine-checkable proof objects as formal correctness certificates.




  • 2016 to present (expected May 2023). PhD student. University of Illinois Urbana-Champaign, USA
  • 2015 to 2016. Research assistant. Singapore University of Technology and Design, Singapore
  • 2014 to 2015. Assistant lecturer. Birmingham City University, UK
  • 2010 to 2014. B.S., Peking University, China


  • Graduate College’s Dissertation Completion Fellowship (2022)
  • Mavis Future Faculty Fellow (2020)
  • Yunni & Maxine Pao Memorial Fellowship (2018-2019)
  • China National Scholarship (2012-2013)

Selected Publications

  1. Towards a trustworthy semantics-based language framework via proof generation
    Chen, Xiaohong, Lin, Zhengyao, Trinh, Minh-Thai, and Roşu, Grigore
    In Proceedings of CAV 2021
  2. A general approach to define binders using matching logic
    Chen, Xiaohong, and Roşu, Grigore
    In Proceedings of ICFP 2020
  3. Towards A unified proof framework for automated fixpoint reasoning using matching logic
    Chen, Xiaohong, Trinh, Minh-Thai, Rodrigues, Nishant, Peña, Lucas, and Roşu, Grigore
    In Proceedings of OOPSLA 2020
  4. Matching μ-logic
    Chen, Xiaohong, and Roşu, Grigore
    In Proceedings of LICS 2019