Functional description extraction of code based on formal semantics of Clight
WANG Tao CHEN Min-yi QI Jun
Journal of Computer Applications . 2012, (08): 2333 -2337 .  DOI: 10.3724/SP.J.1087.2012.02333