| 2025 | ESOP | A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model. | Weijie Fan, Hongjin Liang, Xinyu Feng, Hanru Jiang |
| 2025 | ESOP | Verifying Algorithmic Versions of the Lovsz Local Lemma. | Rongen Lin, Hongjin Liang, Xinyu Feng |
| 2025 | SETTA | A Program Logic for Byzantine-Fault-Tolerant Protocols. | Yuwen Kuang, Hongjin Liang, Xinyu Feng |
| 2024 | TASE | Verified Validation for Affine Scheduling in Polyhedral Compilation. | Xuyang Li, Hongjin Liang, Xinyu Feng |
| 2022 | PLDI | Verifying optimizations of concurrent programs in the promising semantics. | Junpeng Zha, Hongjin Liang, Xinyu Feng |
| 2021 | PLDI | Abstraction for conflict-free replicated data types. | Hongjin Liang, Xinyu Feng |
| 2019 | PLDI | Towards certified separate compilation for concurrent programs. | Hanru Jiang, Hongjin Liang, Siyang Xiao, Junpeng Zha, Xinyu Feng |
| 2018 | ICTAC | Non-preemptive Semantics for Data-Race-Free Programs. | Siyang Xiao, Hanru Jiang, Hongjin Liang, Xinyu Feng |
| 2016 | POPL | A program logic for concurrent objects under fair scheduling. | Hongjin Liang, Xinyu Feng |
| 2014 | CSL | Compositional verification of termination-preserving refinement of concurrent programs. | Hongjin Liang, Xinyu Feng, Zhong Shao |
| 2013 | CONCUR | Characterizing Progress Properties of Concurrent Objects via Contextual Refinements. | Hongjin Liang, Jan Hoffmann, Xinyu Feng, Zhong Shao |
| 2013 | PLDI | Modular verification of linearizability with non-fixed linearization points. | Hongjin Liang, Xinyu Feng |
| 2012 | POPL | A rely-guarantee-based simulation for verifying concurrent program transformations. | Hongjin Liang, Xinyu Feng, Ming Fu |