Xiaohong Chen

• ✉
• 𝕏
• ✈
• in

Welcome. I'm the CTO of Pi Squared Inc.

My research focuses on matching logic, a unified foundation for programming language semantics and formal verification. At Pi Squared, I'm building tools that enable universal trust through proof generation and verification.

Bio

• 2024–presentCTOPi Squared Inc.
• 2023–2024Research EngineerRuntime Verification Inc.
• 2016–2023PhDUniversity of Illinois Urbana-Champaign
• 2015–2016Research AssistantSingapore University of Technology and Design
• 2014–2015Assistant LecturerBirmingham City University
• 2010–2014BScPeking University

Selected Publications

• Matching μ-logic.
  Xiaohong Chen.
  PhD Thesis, University of Illinois Urbana-Champaign, 2023.
• Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier.
  Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu.
  OOPSLA 2023. [DOI]
• Towards a Trustworthy Semantics-Based Language Framework via Proof Generation.
  Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu.
  CAV 2021. [DOI]
• A General Approach to Define Binders Using Matching Logic.
  Xiaohong Chen, Grigore Rosu.
  ICFP 2020. [DOI]
• Towards a Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic.
  Xiaohong Chen, Minh-Thai Trinh, Nishant Rodrigues, Lucas Peña, Grigore Rosu.
  OOPSLA 2020. [DOI]
• Matching μ-Logic.
  Xiaohong Chen, Grigore Rosu.
  LICS 2019. [DOI]

View all publications →