Quasi-Linearizability is Undecidable. - Chao Wang 069; Yi Lv; Gaoang Liu; Peng Wu 002 (APLAS, 2015)

Bounded TSO-to-SC Linearizability Is Decidable. - Chao Wang 069; Yi Lv; Peng Wu 002 (SOFSEM, 2016)

Checking Linearizability of Concurrent Priority Queues. - Ahmed Bouajjani; Constantin Enea; Chao Wang 069 (CONCUR, 2017)

Decomposable Relaxation for Concurrent Data Structures. - Chao Wang 069; Yi Lv; Peng Wu 002 (SOFSEM, 2017)

TSO-to-TSO linearizability is undecidable. - Chao Wang 069; Yi Lv; Peng Wu 002 (Acta Informatica, 2018)

Decidability of linearizabilities for relaxed data structures. - Chao Wang 069; Yi Lv; Peng Wu 002 (Sci. China Inf. Sci., 2018)

Replication-aware linearizability. - Chao Wang 069; Constantin Enea; Suha Orhun Mutluergil; Gustavo Petri (PLDI, 2019)

Decidability of Liveness on the TSO Memory Model. - Chao Wang 069; Gustavo Petri; Yi Lv; Teng Long; Zhiming Liu 001 (CoRR, 2021)

A Contract-Based Semantics and Refinement for Simulink. - Quan Sun; Wei Zhang; Chao Wang 069; Zhiming Liu 001 (SETTA, 2022)

Decidability of Liveness for Concurrent Objects on the TSO Memory Model. - Chao Wang 069; Gustavo Petri; Yi Lv; Teng Long; Zhiming Liu 001 (SETTA, 2022)

VeriLin: A Linearizability Checker for Large-Scale Concurrent Objects. - Qiaowen Jia; Yi Lv; Peng Wu 002; Bohua Zhan; Jifeng Hao; Hong Ye; Chao Wang 069 (TASE, 2023)

Towards correctness proof for hybrid Simulink block diagrams. - Wei Zhang; Quan Sun; Chao Wang 069; Zhiming Liu 001 (J. Syst. Archit., 2023)

A contract-based semantics and refinement for hybrid Simulink block diagrams. - Quan Sun; Wei Zhang; Chao Wang 069; Zhiming Liu 001 (J. Syst. Archit., 2023)

Universal Construction for Linearizable but Not Strongly Linearizable Concurrent Objects. - Chao Wang 069; Peng Wu 002; Gustavo Petri; Qiaowen Jia; Youlin He; Yi Lv; Zhiming Liu 001 (SETTA, 2024)