Xiaohong Chen

[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.

Contact

xc3@illinois.edu

Bio

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

Awards

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

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

Abs TechRep PDF

A language-agnostic program verifier takes as input both a program with its formal specification and the formal semantics of the programming language in which the program is written, and then uses a language-agnostic verification algorithm to prove the program correct with respect to its specification, using directly the formal language semantics. Such a complex verifier can easily have bugs. This paper proposes a method to certify the correctness of each successful verification run by generating a proof certificate for it. The proof certificate can be checked by a small proof checker. The preliminary experiments apply the method to generate proof certificates for the verification of an imperative language, a functional language, and a virtual machine language, showing that the proposed method is language-agnostic.
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

Abs doi PDF Slides

We pursue the vision of an ideal language framework, where programming language designers only need to define the formal syntax and semantics of their languages, and all language tools are automatically generated by the framework. Due to the complexity of such a language framework, it is a big challenge to ensure its trustworthiness and to establish the correctness of the autogenerated language tools. In this paper, we propose an innovative approach based on proof generation. The key idea is to generate proof objects as correctness certificates for each individual task that the language tools conduct, on a case-by-case basis, and use a trustworthy proof checker to check the proof objects. This way, we avoid formally verifying the entire framework, which is practically impossible, and thus can make the language framework both practical and trustworthy. As a first step, we formalize program execution as mathematical proofs and generate their complete proof objects. The experimental result shows that the performance of our proof object generation and proof checking is very promising.
A general approach to define binders using matching logic

Chen, Xiaohong, and Roşu, Grigore

In Proceedings of ICFP 2020

Abs doi TALK TechRep PDF Slides

We propose a novel definition of binders using matching logic, where the binding behavior of object-level binders is directly inherited from the built-in exists binder of matching logic. We show that the behavior of binders in various logical systems such as lambda-calculus, System F, pi-calculus, pure type systems, can be axiomatically defined in matching logic as notations and logical theories. We show the correctness of our definitions by proving conservative extension theorems, which state that a sequent/judgment is provable in the original system if and only if it is provable in matching logic, in the corresponding theory. Our matching logic definition of binders also yields models to all binders, which are deductively complete with respect to formal reasoning in the original systems. For lambda-calculus, we further show that the yielded models are representationally complete, a desired property that is not enjoyed by many existing lambda-calculus semantics. This work is part of a larger effort to develop a logical foundation for the programming language semantics framework K (http://kframework.org).
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

Abs doi TALK PDF Slides

Automation of fixpoint reasoning has been extensively studied for various mathematical structures, logical formalisms, and computational domains, resulting in specialized fixpoint provers for heaps, for streams, for term algebras, for temporal properties, for program correctness, and for many other formal systems and inductive and coinductive properties. However, in spite of great theoretical and practical interest, there is no unified framework for automated fixpoint reasoning. Although several attempts have been made, there is no evidence that such a unified framework is possible, or practical. In this paper, we propose a candidate based on matching logic, a formalism recently shown to theoretically unify the above mentioned formal systems. Unfortunately, the (Knaster-Tarski) proof rule of matching logic, which enables inductive reasoning, is not syntax-driven. Worse, it can be applied at any step during a proof, making automation seem hopeless. Inspired by recent advances in automation of inductive proofs in separation logic, we propose an alternative proof system for matching logic, which is amenable for automation. We then discuss our implementation of it, which although not superior to specialized state-of-the-art automated provers for specific domains, we believe brings some evidence and hope that a unified framework for automated reasoning is not out of reach.
Matching μ-logic

Chen, Xiaohong, and Roşu, Grigore

In Proceedings of LICS 2019

Abs doi TechRep PDF Slides

Matching logic is a logic for specifying and reasoning about structure by means of patterns and pattern matching. This paper makes two contributions. First, it proposes a sound and complete proof system for matching logic in its full generality. Previously, sound and complete deduction for matching logic was known only for particular theories providing equality and membership. Second, it proposes matching μ-logic, an extension of matching logic with a least fixpoint μ-binder. It is shown that matching μ-logic captures as special instances many important logics in mathematics and computer science, including first-order logic with least fixpoints, modal mu-logic as well as dynamic logic and various temporal logics such as infinite/finite-trace linear temporal logic and computation tree logic, and notably reachability logic, the underlying logic of the K framework for programming language semantics and formal analysis. Matching μ-logic therefore serves as a unifying foundation for specifying and reasoning about fixpoints and induction, programming languages and program specification and verification.