堆栈机器简单编译器在Isabelle/HOL中的验证

陈飞扬; 徐文涛; 孙绍山; 朱浩; 钱振江

首页> 中文期刊> 《常熟理工学院学报》 >堆栈机器简单编译器在Isabelle/HOL中的验证

堆栈机器简单编译器在Isabelle/HOL中的验证

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

堆栈机器(stack machine)作为一种计算模型,不仅执行部分高级语言的效率很高,而且其编译器也简单、快速.在形式化领域,目前已有不少定理证明器用来验证模型的正确性.本文对堆栈机器的简单编译器进行介绍,对布尔表达式和算术表达式、机器指令、编译器、机器运行行为在Isabelle/HOL中进行形式化,验证编译器的正确性.

著录项

来源
《常熟理工学院学报》 |2019年第5期|43-46|共4页
作者
陈飞扬; 徐文涛; 孙绍山; 朱浩; 钱振江;
展开▼
作者单位

常熟理工学院计算机科学与工程学院;

江苏常熟 215500;

常熟理工学院计算机科学与工程学院;

江苏常熟 215500;

常熟理工学院计算机科学与工程学院;

江苏常熟 215500;

常熟理工学院计算机科学与工程学院;

江苏常熟 215500;

常熟理工学院计算机科学与工程学院;

江苏常熟 215500;

展开▼
原文格式 PDF
正文语种 chi
中图分类理论、方法;
关键词
堆栈机器; 编译器; 定理证明器; 形式化方法; Isabelle/HOL;

相似文献

中文文献
外文文献
专利

1. 文件比较算法fcomp在Isabelle/HOL中的验证 [J] . 宋丽华 ,王海涛 ,季晓君 . 软件学报 . 2017,第002期
2. SAODV协议在Isabelle/HOL中的正确性验证 [J] . 王金双 ,杨华兵 ,张兴元 . 解放军理工大学学报（自然科学版） . 2008,第005期
3. 一种基于Isabelle/HOL的安全通信协议验证方法 [J] . 夏锐 ,钱振江 ,刘苇 . 计算机工程 . 2021,第001期
4. 基于Isabelle/HOL的安全操作系统形式化验证方法 [J] . 郭毅 ,杨维永 ,刘苇 . 计算机与现代化 . 2017,第004期
5. VSOS-HAM:基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究 [J] . 钱振江 ,黄皓 ,宋方敏 . 南京大学学报：自然科学版 . 2017,第3期
6. SAODV协议在Isabelle/HOL中的正确性验证 [C] . . 第十六届全国网络与数据通信学术会议(NDCC2008) . 2008
7. 基于Isabelle/HOL的Linux 0.11内核调度模块形式化设计与验证研究 [A] . 杜雨晴 . 2015

堆栈机器简单编译器在Isabelle/HOL中的验证

摘要

著录项

相似文献

相关主题

期刊订阅