Splitting Theory of C Programming Language

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

Together with my collaborator Tony Zhou, 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.

We formalized the control flow of C programs without concurrency assumptions and completed the soundness proof in Coq.