Formal Verification of <sub>m</sub>Java Compiler Targeting Micro-Dalvik Virtual Machine

JIANG Nan; HE Yan-xiang; ZHANG Xiao-tong

doi:10.3969/j.issn.0372-2112.2016.07.015

您当前的位置：

首页 >

文章列表页 >

Formal Verification of _mJava Compiler Targeting Micro-Dalvik Virtual Machine

更新时间：2025-07-16

- Formal Verification of _mJava Compiler Targeting Micro-Dalvik Virtual Machine
- Acta Electronica Sinica Vol. 44, Issue 7, Pages: 1619-1629(2016)
- 作者机构：
  
  1. 武汉大学计算机学院,湖北,武汉,430072
  2. 武汉大学软件工程国家重点实验室,湖北,武汉,430072
  3. 湖北工业大学计算机学院,湖北,武汉,430070
  4. 武汉大学计算机学院,湖北,武汉,430072
  5. 武汉大学软件工程国家重点实验室,湖北,武汉,430072
  6. 湖北工业大学计算机学院,湖北,武汉,430070
- 作者简介：
- 基金信息：
  
  National Natural Science Foundation of China (No.61373039)
- DOI：10.3969/j.issn.0372-2112.2016.07.015
  CLC： TP311
- Published Online：25 July 2016，
  
  Published：2016
- 稿件说明：
移动端阅览
JIANG Nan, HE Yan-xiang, ZHANG Xiao-tong. Formal Verification of _mJava Compiler Targeting Micro-Dalvik Virtual Machine[J]. Acta Electronica Sinica, 2016, 44(7): 1619-1629.
DOI：

JIANG Nan, HE Yan-xiang, ZHANG Xiao-tong. Formal Verification of _mJava Compiler Targeting Micro-Dalvik Virtual Machine[J]. Acta Electronica Sinica, 2016, 44(7): 1619-1629. DOI： 10.3969/j.issn.0372-2112.2016.07.015.

摘要

针对类Java的面向对象语言

Java到类Dalvik的寄存器架构虚拟机Micro-Dalvik的编译验证

给出了

Java语言和Micro-Dalvik的操作语义.从

Java语言程序到Micro-Dalvik虚拟机指令的编译分为两步

首先将

Java语言程序中的本地变量名转换为相应的序号

得到一个中间语言程序

再将该中间语言程序翻译成Micro-Dalvik虚拟机指令程序.在给出中间语言的操作语义后

构造了

Java语言程序与编译后的中间语言程序的语义保持定理并证明

以及构造了中间语言程序的语义与编译后的Micro-Dalvik虚拟机程序的语义保持定理并证明.整个形式化编译验证在定理证明助手Isabelle/HOL中进行了机器检测.

Java语言和Micro-Dalvik虚拟机分别对Java语言和Dalvik虚拟机进行了抽象

是我们兼顾语言的真实性和形式化的清晰性的结果.但是

所有形式化的语义严格遵从语言规范中的定义

并与Dalvik VM的实现保持一致

从这种意义上讲

该编译器并不是一个实验性质的假想编译器

而是有其实用意义的.

Abstract

This paper introduces a formal verification of

Java compiler targeting Micro-Dalvik virtual machine(VM) where

Java is an object-oriented language similar to Java

and Micro-Dalvik is a Dalvik-like VM of the register-based architecture.The operational semantics of

Java and Micro-Dalvik VM are defined.The compiler operates in two stages.First it replaces the names of local variables by their corresponding indice

s and hence translates

Java into an intermediate language.Then it generates the Micro-Dalvik VM instructions.After defining the operational semantics of the intermediate language

the correctness of the two stages are formulated in terms of the preservation of the semantics and is proved respectively.The whole formalization is machine-checked in the theorem proof assistant Isabelle/HOL.The

Java language and Micro-Dalvik VM are more abstract than the comparable Java and the Dalvik VM

respectively

which is a result of a compromise between the the realism of the language and the clarity of the formalization.However

Java language and Micro-Dalvik VM exhibit core features of an object-oriented programming language and a register-based architecture

respectively

and thus in this sense

this verified compiler is non-trivial.

关键词

Keywords

references

Views

398

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Verifying Implementation Correctness of Compiling Optimization Based on Simulation Relation

Research on Method of Formal Design and Verification of Memory Management Based on Microkernel Architecture

Related Author

XU Chao

HE Yan-xiang

WU Wei

CHEN Yong

LIU Jian-bo

QIAN Zhen-jiang

LIU Yong-jun

YAO Yu-feng

Related Institution

Wuhan University Computer of School

Xuzhou College of Industrial Technology

State Key Laboratory of Software Engineering

Wuhan University Computer of SchoolWuhanHubei 430072China

Xuzhou College of Industrial TechnologyXuzhouJiangsu 221000China

⁰

Formal Verification of mJava Compiler Targeting Micro-Dalvik Virtual Machine

DOI：10.3969/j.issn.0372-2112.2016.07.015

摘要

Abstract

关键词

Keywords

references

Formal Verification of _mJava Compiler Targeting Micro-Dalvik Virtual Machine