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)
Generating proof certificates for a language-agnostic deductive program verifierIn Proceedings of OOPSLA (To Appear) 2023
Towards a trustworthy semantics-based language framework via proof generationIn Proceedings of CAV 2021
A general approach to define binders using matching logicIn Proceedings of ICFP 2020
Towards A unified proof framework for automated fixpoint reasoning using matching logicIn Proceedings of OOPSLA 2020
Matching μ-logicIn Proceedings of LICS 2019