一个机器检测的Micro-Dalvik虚拟机模型?

• 作者: 何炎祥 张军 李清安 江南 沈凡凡
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 大步操作语义 形式化验证 定理证明 寄存器架构的虚拟机
• 年，卷（期）: 2015,（2）
• 页码范围: 364-379
• 页数: 16页
• 分类号: TP303
• 字数: 9368字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004787

摘要

给出了一个寄存器架构的虚拟机模型 Micro-Dalvik,包括虚拟机指令集和虚拟机运行时状态的形式化,并以大步操作语义(big-step operational semantics)的方式给出了指令单步执行的状态转换以及定义在单步执行上的自反传递闭包来表达虚拟机程序的运行时状态转换。最后,以定理的形式描述了语义满足的性质,并得到证明。这个模型的指令集包括了大部分Dalvik虚拟机指令,为获得形式语义的清晰化,它在Dalvik VM指令集上进行了必要的抽象,对其实质没有改变,因而具有较大的实用性。该形式化模型通过了定理证明助手Isabelle/HOL的验证。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	江南	武汉大学计算机学院	18	70	4.0	8.0
3	何炎祥	武汉大学计算机学院	11	71	6.0	8.0
7	张军	武汉大学计算机学院	110	723	13.0	23.0
11	沈凡凡	武汉大学计算机学院	7	37	4.0	6.0
14	李清安	武汉大学计算机学院	18	35	5.0	5.0