论文部分内容阅读
字节码既是运行于虚拟机的解释指令，也是定义良好的中间表示，是当今网络软件和计算设备中广泛使用的重要技术．字节码验证可以提高相关软件的可信程度，同时为构造证明保持编译器提供中间表示支持，具有重要的实用价值和理论价值．虽然近年提出了一些用于字节码程序的逻辑系统，但由于字节码本身的特点，造成了抽象控制栈复杂、控制流结构信息不足，因而字节码程序的“模块化验证”依然是一个巨大的挑战，并没有得到有效解决．将FPCC（foundational proof-carrying code）方法引入中间表示字节码，借鉴汇编程序