Armada: low-effort verification of high-performance concurrent programs. - Jacob R. Lorch; Yixuan Chen 002; Manos Kapritsos; Bryan Parno; Shaz Qadeer; Upamanyu Sharma; James R. Wilcox; Xueyuan Zhao (PLDI, 2020)

Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility. - Jacob R. Lorch; Yixuan Chen 002; Manos Kapritsos; Haojun Ma; Bryan Parno; Shaz Qadeer; Upamanyu Sharma; James R. Wilcox; Xueyuan Zhao (ACM Trans. Program. Lang. Syst., 2022)

A Compositional Theory of Linearizability. - Arthur Oliveira Vale; Zhong Shao 001; Yixuan Chen 002 (Proc. ACM Program. Lang., 2023)

Compositionality and Observational Refinement for Linearizability with Crashes. - Arthur Oliveira Vale; Zhongye Wang; Yixuan Chen 002; Peixin You; Zhong Shao 001 (Proc. ACM Program. Lang., 2024)