A rely-guarantee-based simulation for verifying concurrent program transformations. - Hongjin Liang 001; Xinyu Feng 001; Ming Fu (POPL, 2012)

Characterizing Progress Properties of Concurrent Objects via Contextual Refinements. - Hongjin Liang 001; Jan Hoffmann 002; Xinyu Feng 001; Zhong Shao 001 (CONCUR, 2013)

Modular verification of linearizability with non-fixed linearization points. - Hongjin Liang 001; Xinyu Feng 001 (PLDI, 2013)

Compositional verification of termination-preserving refinement of concurrent programs. - Hongjin Liang 001; Xinyu Feng 001; Zhong Shao 001 (CSL-LICS, 2014)

Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations. - Hongjin Liang 001; Xinyu Feng 001; Ming Fu (ACM Trans. Program. Lang. Syst., 2014)

A program logic for concurrent objects under fair scheduling. - Hongjin Liang 001; Xinyu Feng 001 (POPL, 2016)

Non-preemptive Semantics for Data-Race-Free Programs. - Siyang Xiao; Hanru Jiang; Hongjin Liang 001; Xinyu Feng 001 (ICTAC, 2018)

Progress of concurrent objects with partial methods. - Hongjin Liang 001; Xinyu Feng 001 (Proc. ACM Program. Lang., 2018)

Towards certified separate compilation for concurrent programs. - Hanru Jiang; Hongjin Liang 001; Siyang Xiao; Junpeng Zha; Xinyu Feng 001 (PLDI, 2019)

Progress of Concurrent Objects. - Hongjin Liang 001; Xinyu Feng 001 (Found. Trends Program. Lang., 2020)

Abstraction for conflict-free replicated data types. - Hongjin Liang 001; Xinyu Feng 001 (PLDI, 2021)

Verifying optimizations of concurrent programs in the promising semantics. - Junpeng Zha; Hongjin Liang 001; Xinyu Feng 001 (PLDI, 2022)

Verified Validation for Affine Scheduling in Polyhedral Compilation. - Xuyang Li; Hongjin Liang 001; Xinyu Feng 001 (TASE, 2024)

A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model. - Weijie Fan; Hongjin Liang 001; Xinyu Feng 001; Hanru Jiang (ESOP (1), 2025)

Verifying Algorithmic Versions of the Lovász Local Lemma. - Rongen Lin; Hongjin Liang 001; Xinyu Feng 001 (ESOP (1), 2025)