Runtime Verification by Convergent Formula Progression. - Yan Shen; Jianwen Li; Zheng Wang 005; Ting Su 001; Bin Fang 004; Geguang Pu; Wanwei Liu; Mingsong Chen 001 (APSEC (1), 2014)

Automated Coverage-Driven Test Data Generation Using Dynamic Symbolic Execution. - Ting Su 001; Geguang Pu; Bin Fang 004; Jifeng He 001; Jun Yan; Siyuan Jiang; Jianjun Zhao 001 (SERE, 2014)

Formal Development of a Real-Time Operating System Memory Manager. - Wen Su; Jean-Raymond Abrial; Geguang Pu; Bin Fang 004 (ICECCS, 2015)

Hierarchical Shape Abstraction for Analysis of Free List Memory Allocators. - Bin Fang 004; Mihaela Sighireanu (LOPSTR, 2016)

A refinement hierarchy for free list memory allocators. - Bin Fang 004; Mihaela Sighireanu (ISMM, 2017)

Formal modelling of list based dynamic memory allocators. - Bin Fang 004; Mihaela Sighireanu; Geguang Pu; Wen Su; Jean-Raymond Abrial; Mengfei Yang; Lei Qiao 002 (Sci. China Inf. Sci., 2018)

Techniques for formal modelling and verification on dynamic memory allocators. (Techniques de modélisation et de vérification formelles des allocateurs de mémoire dynamiques). - Bin Fang 004 (2018)