Invariant Synthesis for Programs Manipulating Arrays with Unbounded Data. - Bin Li 054; Zhenhao Tang; Jianhua Zhao (Internetware, 2015)

Analyzing Inductively Defined Properties for Recursive Data Structures. - Zhenhao Tang; Hanfei Wang; Bin Li 054; Juan Zhai; Jianhua Zhao; Xuandong Li (Internetware, 2015)

Code Generation for Abstract Data Types Based on Program Analysis. - Bin Li 054; Jun Liu; Jianhua Zhao (QRS Companion, 2015)

Node-Set Analysis for Linked Recursive Data Structures. - Zhenhao Tang; Hanfei Wang; Bin Li 054; Juan Zhai; Jianhua Zhao; Xuandong Li (QRS, 2015)

Automatic Invariant Synthesis for Arrays in Simple Programs. - Bin Li 054; Zhenhao Tang; Juan Zhai; Jianhua Zhao (QRS, 2016)

Precondition Calculation for Loops Iterating over Data Structures. - Juan Zhai; Bin Li 054; Zhenhao Tang; Jianhua Zhao; Xuandong Li (QRS, 2016)

A Framework for Array Invariants Synthesis in Induction-Loop Programs. - Bin Li 054; Juan Zhai; Zhenhao Tang; Enyi Tang; Jianhua Zhao (APSEC, 2017)

Are Your Classes Well-Encapsulated? Encapsulation Analysis for Java. - Zhenhao Tang; Juan Zhai; Bin Li 054; Jianhua Zhao (QRS, 2017)