About Me

I’m currently a master student in Software Engineering Institute at East China Normal University(ECNU) since 2022, advised by Prof. Geguang Pu and Prof. Jianwen Li.

My current research interests revolve around solving real challenges using formal verification techniques, with a particular focus on model checking and SAT. At present, I am deeply engaged in the development of Complementary Approximate Reachability(CAR), a cutting-edge safety model checking algorithm. This involves not only refining the algorithm but also creating novel implementations and applying it to real-world problem-solving.

Before joining ECNU, I spent my undergraduate time at Shanghai Jiao Tong University(SJTU). I worked around compiler correctness and mathematical logic in Coq, the proof assistant, under supervision of Prof. Qinxiang Cao.

I am currently actively seeking a PhD position that aligns with my research interests and passion.

For my detailed CV, ping me.

Publications

• LightF3: A Lightweight Fully-Process Formal Framework for Automated Verifying Railway Interlocking Systems link
• More in-progress…

Research Experience

Graduate

Some paper are in progress. Relevant information is marked as ███ .

Accelerating CAR-Based Model Checking with █████ ████ ████

Jan.2024 – June. 2024 Supervised by Ofer Strichman from Technion and Jianwen Li from ECNU.

In SAT-based model checking, a key component is the ████████████████████████.

We suggested several performance improvements to this process, most notably a technique for ████████████████.

Our results showed that my implementation of these techniques, not only improved its performance, but also solved more unsafe cases than any other model-checker in the public domain, including █ unique instances from the HWMCC that were previously unsolved.

Revisiting ██████ in CAR-Based Model Checking

July. 2023 – Dec. 2024 Supervised by Ofer Strichman from Technion and Jianwen Li from ECNU

We found that the performance of model checkers are sensitive to ████████████████.

We analyzed the reason theoretically, extended existing strategies and finally proposed new ones. The implementation of the new strategies could not only outperforms other strategies, but also outperforms other state-of-the-art bug-finding algorithms .

Formal Verification of Interlocking Systems

June.2022 – June.2023 Supervised by Jianwen Li and Geguang Pu from ECNU

See: Talk, Demo, Paper

The formal verification of interlocking systems has long been a open problem due to the complexity of domain knowledge.

With the help of our industrial partner, I designed a Domain Specific Language RIS-FL and implemented LightF3, a formal framework for verifying railway interlocking systems and evaluated it with real station instances from our industrial partner, demonstrating its effectiveness. With its help, we successfully found deep hidden bugs in existing designs.

Our paper was accepted by FSE’23(The ACM International Conference on the Foundations of Software Engineering).

Undergraduate

Splitting Theory of C Programming Language

Jan. 2020 – Jan. 2021 Supervised by QinXiang Cao from SJTU.

We designed a decomposition theory for C programs based on Hoare logic, allowing us to generate the necessary Hoare Triples for a given C program.

Together with my collaborator, we formalized the control flow of C programs without concurrency assumptions and completed the soundness proof in Coq.

An Annotated variant CompCert-Clightgen

Oct. 2019 – Jan. 2020 Supervised by QinXiang Cao from SJTU

In CompCert, the verified compiler, Clightgen can automatically generate the correctness proofs (written in Coq) that need to be done for C programs.

My work aimed to allow users to provide auxiliary proof information in the form of comments within the C program, thereby enabling VST to automatically complete the proofs. I extended the annotation syntax based on a basic version of VST-A, implemented the collection and parsing of out-of-function annotations on the Clight syntax tree, and ultimately generated the corresponding Coq commands automatically.

Based on this, we made a demo that enables interpretive verification of annotation C programs called VST-IDE.

Automatic Correcting of Basic Math Proofs

Mar. 2019 – Sept. 2019 Supervised by QinXiang Cao from SJTU

Our work aimed to design an automatic grading tool for mathematical proofs written with Chinese keywords. This tool reads mathematical proofs concerning the properties of limits written in Chinese and Markdown formulas and validates them.

I was responsible for designing the parser for mathematical proofs with Chinese keywords and implementing the translation from input to formal proofs in Coq. By leveraging Coq library components developed by collaborators, we achieved automatic grading. We completed a demo and presented it internally within the lab.