Formal Verification of Scalable NonZero Indicators. - Shao Jie Zhang; Yang Liu 003; Jun Sun 001; Jin Song Dong; Wei Chen 013; Yanhong A. Liu (SEKE, 2009)

Model Checking a Lazy Concurrent List-Based Set Algorithm. - Shao Jie Zhang; Yang Liu 003 (SSIRI, 2010)

An Automatic Approach to Model Checking UML State Machines. - Shao Jie Zhang; Yang Liu 003 (SSIRI (Companion), 2010)

On Combining State Space Reductions with Global Fairness Assumptions. - Shao Jie Zhang; Jun Sun 001; Jun Pang 001; Yang Liu 003; Jin Song Dong (FM, 2011)

Scalable automatic linearizability checking. - Shao Jie Zhang (ICSE, 2011)

Graph-based detection of library API imitations. - Chengnian Sun; Siau-Cheng Khoo; Shao Jie Zhang (ICSM, 2011)

Constraint-based automatic symmetry detection. - Shao Jie Zhang; Jun Sun 001; Chengnian Sun; Yang Liu 003; Junwei Ma; Jin Song Dong (ASE, 2013)

Verifying Linearizability via Optimized Refinement Checking. - Yang Liu 003; Wei Chen 013; Yanhong A. Liu; Jun Sun 001; Shao Jie Zhang; Jin Song Dong (IEEE Trans. Software Eng., 2013)

Formal Verification of Operational Transformation. - Yang Liu 003; Yi Xu; Shao Jie Zhang; Chengzheng Sun (FM, 2014)

Model checking with fairness assumptions using PAT. - Yuanjie Si; Jun Sun 001; Yang Liu 003; Jin Song Dong; Jun Pang 001; Shao Jie Zhang; Xiaohu Yang 001 (Frontiers Comput. Sci., 2014)

Verifying a quantitative relaxation of linearizability via refinement. - Kiran Adhikari; James Street; Chao Wang 001; Yang Liu 003; Shao Jie Zhang (Int. J. Softw. Tools Technol. Transf., 2016)