Publications

Matching μ-logic.
Xiaohong Chen.
PhD Thesis, University of Illinois Urbana-Champaign, 2023.

𝕂 Definitions as Matching Logic Theories, Formally.
Xiaohong Chen, Horațiu Cheval, Dorel Lucanu, Grigore Roșu.
FoSSaCS 2026, pp. 198-219. [DOI]
A Matching Logic Theory of Multi-hole Contexts.
Xiaohong Chen, Horațiu Cheval, Dorel Lucanu, Grigore Roșu.
Journal of Logical and Algebraic Methods in Programming, Article 101151, 2026. [DOI]
A Unifying Logical Foundation for Initial Algebra Semantics and Induction.
Xiaohong Chen, Dorel Lucanu, Grigore Rosu.
Theoretical Computer Science, Article 115981, 2026. [DOI]

Actors and Blockchains, Together.
Xiaohong Chen, Grigore Rosu.
Concurrent Programming, Open Systems and Formal Methods, pp. 215-236, 2025. [DOI]
FastSet: Parallel Claim Settlement.
Xiaohong Chen, Grigore Rosu.
arXiv preprint, 2025. [arXiv]

A Logical Treatment of Finite Automata.
Nishant Rodrigues, Mircea Sebe, Xiaohong Chen, Grigore Rosu.
TACAS 2024, pp. 350-369. [DOI]

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier.
Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu.
OOPSLA 2023, pp. 56-84. [DOI]
Capturing Constrained Constructor Patterns in Matching Logic.
Xiaohong Chen, Dorel Lucanu, Grigore Rosu.
Journal of Logical and Algebraic Methods in Programming, vol. 130, 2023.

Rewriting-Based Computer-Interpretable Clinical Practice Guidelines.
Manasvi Saxena, Xiaohong Chen, Shuang Song, Shaoyu Meng, Lui Sha, Grigore Rosu.
Technical Report, University of Illinois Urbana-Champaign, 2022. [IDEALS]
Towards a Unifying Logical Framework for Neural Networks.
Xiyue Zhang, Xiaohong Chen, Meng Sun.
ICTAC 2022, pp. 442-461. [DOI]
Mechanizing Matching Logic in Coq.
Péter Bereczky, Xiaohong Chen, Dániel Horpácsi, Tamás Bálint Mizsei, Lucas Peña, Jan Tusil.
FROM 2022, pp. 17-36. [DOI]

Towards a Trustworthy Semantics-Based Language Framework via Proof Generation.
Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu.
CAV 2021, pp. 477-499. [DOI]
Matching Logic Explained.
Xiaohong Chen, Dorel Lucanu, Grigore Rosu.
Journal of Logical and Algebraic Methods in Programming, vol. 120, 2021. [DOI]

A General Approach to Define Binders Using Matching Logic.
Xiaohong Chen, Grigore Rosu.
ICFP 2020, pp. 88:1-88:32. [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, pp. 161:1-161:29. [DOI]
Connecting Constrained Constructor Patterns and Matching Logic.
Xiaohong Chen, Dorel Lucanu, Grigore Rosu.
WRLA 2020, pp. 19-37. [DOI]

Matching μ-Logic.
Xiaohong Chen, Grigore Rosu.
LICS 2019, pp. 1-13. [DOI]
Matching μ-Logic: Foundation of K Framework.
Xiaohong Chen, Grigore Rosu.
CALCO 2019 (Invited Paper), pp. 1:1-1:4. [DOI]
K - A Semantic Framework for Programming Languages and Formal Analysis.
Xiaohong Chen, Grigore Rosu.
SETSS 2019, pp. 122-158. [DOI]

A Language-Independent Program Verification Framework.
Xiaohong Chen, Grigore Rosu.
ISoLA 2018, pp. 92-102. [DOI]
A Language-Independent Approach to Smart Contract Verification.
Xiaohong Chen, Daejun Park, Grigore Rosu.
ISoLA 2018, pp. 405-413. [DOI]

Improving Probability Estimation Through Active Probabilistic Model Learning.
Jingyi Wang, Xiaohong Chen, Jun Sun, Shengchao Qin.
ICFEM 2017, pp. 379-395. [DOI]

Towards Concolic Testing for Hybrid Systems.
Pingfan Kong, Yi Li, Xiaohong Chen, Jun Sun, Meng Sun, Jingyi Wang.
FM 2016, pp. 460-478. [DOI]
Component-Based Modelling for Scalable Smart City Systems Interoperability.
Esther Palomar, Xiaohong Chen, Zhiming Liu, Sabita Maharjan, Jonathan P. Bowen.
Sensors, vol. 16(11), 2016. [DOI]

A Framework for Off-Line Conformance Testing of Timed Connectors.
Shaodong Li, Xiaohong Chen, Yiwu Wang, Meng Sun.
TASE 2015, pp. 15-22. [DOI]

A Hybrid Model of Connectors in Cyber-Physical Systems.
Xiaohong Chen, Jun Sun, Meng Sun.
ICFEM 2014, pp. 59-74. [DOI]
Model-Driven Design of Object and Component Systems.
Zhiming Liu, Xiaohong Chen.
SETSS 2014, pp. 152-255. [DOI]