基于Coq的命令式语言编译器机械验证的研究与实现

盛枫; 窦亮; 杨宗源

首页> 中文期刊> 《小型微型计算机系统》 >基于Coq的命令式语言编译器机械验证的研究与实现

基于Coq的命令式语言编译器机械验证的研究与实现

开具论文收录证明 >>

文献代查 >>

页面导航

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

摘要

软件的可靠性和可信性越来越受到人们的关注,而编译器作为软件开发的基础,其正确性的验证一直都是个重要且迫切的问题.设计和实现一个小型命令式语言IMP的编译器,该编译器将IMP源代码转换成定理证明器Coq接受的函数式语言表示形式的代码,通过语义分析得到IMP目标代码,在堆栈中执行得到结果.本文的重点是使用交互式定理证明器Coq机械验证函数式语言表示形式的源代码编译执行前后的属性和行为均保持一致.本文的工作为使用堆栈的编译器和其他软件系统的机械化形式验证提供了一种新的思路和方法.

著录项

来源
《小型微型计算机系统》 |2015年第9期|1927-1931|共5页
作者
盛枫; 窦亮; 杨宗源;
展开▼
作者单位

华东师范大学计算机科学与技术系;

展开▼
原文格式 PDF
正文语种 chi
中图分类编译程序、解释程序;
关键词
定理证明器Coq; 机械验证; 堆栈; 函数式语言;

相似文献

中文文献
外文文献
专利

1. 面向微处理器验证的约束描述语言及其编译器 [J] . 朱丹 ,冷彪 ,李暾 . 计算机工程与应用 . 2005,第019期
2. 基于Coq的操作系统任务管理需求层建模及验证 [J] . 姜菁菁 ,乔磊 ,杨孟飞 . 软件学报 . 2020,第008期
3. 基于Coq的软件安全性验证 [J] . 谯婷婷 ,王乐 ,王芳 . 计算机应用 . 2012,第0z2期
4. 基于Coq的软件安全性验证 [J] . 谯婷婷 ,王乐 ,王芳 . 计算机应用 . 2012,第A02期
5. 基于Coq的微内核操作系统程序验证方法研究 [J] . 张忠秋 ,董云卫 ,张雨 . 计算机测量与控制 . 2011,第008期
6. 一种基于安全C的编译器形式验证方法 [C] . 陈志伟 ,谭宇 . 全国抗恶劣环境计算机第二十六届学术年会 . 2016
7. 基于Coq的软件安全性验证研究与实现 [A] . 王乐 . 2014

基于Coq的命令式语言编译器机械验证的研究与实现

摘要

著录项

相似文献

相关主题

期刊订阅