mJava到Micro-Dalvik虚拟机的编译验证
江南, 何炎祥, 张晓瞳
Formal Verification of mJava Compiler Targeting Micro-Dalvik Virtual Machine
JIANG Nan, HE Yan-xiang, ZHANG Xiao-tong
电子学报 . 2016, (7): 1619 -1629 .  DOI: 10.3969/j.issn.0372-2112.2016.07.015