Symbolic Analysis Tools for CSP. - Liyi Li 002; Elsa L. Gunter; William Mansky (ICTAC, 2014)

A Method to Translate Order-Sorted Algebras to Many-Sorted Algebras. - Liyi Li 002; Elsa L. Gunter (WPTE@FSCD, 2017)

IsaK-Static: A Complete Static Semantics of mathbb K. - Liyi Li 002; Elsa L. Gunter (FACS, 2018)

K-LLVM: A Relatively Complete Semantics of LLVM IR. - Liyi Li 002; Elsa L. Gunter (ECOOP, 2020)

Per-Location Simulation. - Liyi Li 002; Elsa L. Gunter (NFM, 2020)

A verification framework suitable for proving large language translations - Liyi Li 002 (2020)

A Complete Semantics of $ mathbb {K}$ and Its Translation to Isabelle. - Liyi Li 002; Elsa L. Gunter (ICTAC, 2021)

Proving Quantum Programs Correct. - Kesha Hietala; Robert Rand 001; Shih-Han Hung; Liyi Li 002; Michael Hicks 001 (ITP, 2021)

A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm. - Yuxiang Peng; Kesha Hietala; Runzhou Tao; Liyi Li 002; Robert Rand 001; Michael Hicks 001; Xiaodi Wu 001 (CoRR, 2022)

Quantum Natural Proof: A New Perspective of Hybrid Quantum-Classical Program Verification. - Liyi Li 002; Mingwei Zhu; Yi Lee; Le Chang; Xiaodi Wu 001 (CoRR, 2022)

Verified compilation of Quantum oracles. - Liyi Li 002; Finn Voichick; Kesha Hietala; Yuxiang Peng; Xiaodi Wu 001; Michael Hicks 001 (Proc. ACM Program. Lang., 2022)

CheckedCBox: Type Directed Program Partitioning with Checked C for Incremental Spatial Memory Safety. - Liyi Li 002; Arunkumar Bhattar; Le Chang; Mingwei Zhu; Aravind Machiry (CoRR, 2023)

A formal model of Checked C. - Liyi Li 002; Yiyun Liu; Deena L. Postol; Leonidas Lampropoulos; David Van Horn; Michael Hicks 001 (J. Comput. Secur., 2023)

Qunity: A Unified Language for Quantum and Classical Computing. - Finn Voichick; Liyi Li 002; Robert Rand 001; Michael Hicks 001 (Proc. ACM Program. Lang., 2023)

A Verified Optimizer for Quantum Circuits. - Kesha Hietala; Robert Rand 001; Liyi Li 002; Shih-Han Hung; Xiaodi Wu 001; Michael Hicks 001 (ACM Trans. Program. Lang. Syst., 2023)

Qafny: A Quantum-Program Verifier. - Liyi Li 002; Mingwei Zhu; Rance Cleaveland; Alexander Nicolellis; Yi Lee; Le Chang; Xiaodi Wu 001 (ECOOP, 2024)

The Quantum Abstract Machine. - Liyi Li 002; Le Chang; Rance Cleaveland; Mingwei Zhu; Xiaodi Wu 001 (CoRR, 2024)

DisQ: A Markov Decision Process Based Language for Quantum Distributed Systems. - Le Chang; Saitej Yavvari; Rance Cleaveland; Samik Basu 001; Liyi Li 002 (CoRR, 2024)

Qafny: A Quantum-Program Verifier (Artifact). - Liyi Li 002; Mingwei Zhu; Rance Cleaveland; Alexander Nicolellis; Yi Lee; Le Chang; Xiaodi Wu 001 (Dagstuhl Artifacts Ser., 2024)

Validate Quantum State Preparation Programs. - Liyi Li 002; Anshu Sharma; Zoukarneini Difaizi Tagba; Sean Frett; Alex Potanin (CoRR, 2025)