Xiaohong Chen 陈霄泓

Welcome to my homepage. I'm a PhD graduand in Computer Science at the University of Illinois Urbana-Champaign. My research interests are in logic and formal methods, with a focus on improving the trustworthiness of programs, programming language implementations, and formal analysis tools.

[My CV]

[My thesis]

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. Generating proof certificates for a language-agnostic deductive program verifier
    Lin, Zhengyao, Chen, Xiaohong, Trinh, Minh-Thai, Wang, John, and Roşu, Grigore
    In Proceedings of OOPSLA (To Appear) 2023
  2. 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
  3. A general approach to define binders using matching logic
    Chen, Xiaohong, and Roşu, Grigore
    In Proceedings of ICFP 2020
  4. 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
  5. Matching μ-logic
    Chen, Xiaohong, and Roşu, Grigore
    In Proceedings of LICS 2019