Verification of Nondeterministic Quantum Programs. - Yuan Feng 001; Yingte Xu (ASPLOS (3), 2023)

Refinement calculus of quantum programs with projective assertions. - Yuan Feng 001; Li Zhou 013; Yingte Xu (CoRR, 2023)

D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation. - Yingte Xu; Li Zhou 013; Gilles Barthe (CAV (4), 2025)

Automating Equational Proofs in Dirac Notation. - Yingte Xu; Gilles Barthe; Li Zhou 013 (Proc. ACM Program. Lang., 2025)