汇编代码验证中的形式规范自动生成

葛琳; 陈意云; 华保健; 李兆鹏; 刘诚

首页> 中文期刊> 《小型微型计算机系统》 >汇编代码验证中的形式规范自动生成

汇编代码验证中的形式规范自动生成

开具论文收录证明 >>

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

文献代查 >>

页面导航

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

摘要

与传统的高级语言程序验证相比,汇编代码验证中所需要的形式规范往往比较复杂,通常的做法是要求程序员手写形式规范,或是牺牲形式规范的表达能力以期能够自动生成规范.本文提出一种能够自动生成形式规范的方法,该方法依托一个出具证明的编译器自动生成汇编级形式规范,从而减轻程序员的负担.使用该方法生成的规范比现有的其他方法自动生成的规范具有更强的表达能力.文章主要描述该方法在出具证明编译器中的实现.

著录项

来源
《小型微型计算机系统》 |2008年第7期|1219-1224|共6页
作者
葛琳; 陈意云; 华保健; 李兆鹏; 刘诚;
展开▼
作者单位

中国科学技术大学,计算机科学技术系,安徽,合肥,230027;

中国科学技术大学,计算机科学技术系,安徽,合肥,230027;

中国科学技术大学,计算机科学技术系,安徽,合肥,230027;

中国科学技术大学,计算机科学技术系,安徽,合肥,230027;

中国科学技术大学,计算机科学技术系,安徽,合肥,230027;

展开▼
原文格式 PDF
正文语种 chi
中图分类形式语言理论;
关键词
出具证明编译器; 汇编代码验证; 形式规范; Hoare逻辑; 前(后)条件;

相似文献

中文文献
外文文献
专利

1. 通过分析代码覆盖提高功能覆盖率的验证输入自动生成方法 [J] . 傅亮 ,卢鼎 ,张志敏 . 计算机辅助设计与图形学学报 . 2009,第004期
2. DSP应用程序中C代码和汇编代码的结合 [J] . Eran Balaish . 电子与电脑 . 2008,第002期
3. DSP应用程序中C代码和汇编代码的结合 [J] . Eran Balaish . 电子与电脑 . 2008,第002期
4. 代码自动生成技术在实验教学中的应用 [J] . 张磊 . 电气电子教学学报 . 2019,第005期
5. 基于XML的代码自动生成技术在软件开发中的应用 [J] . 武建亮 ,辛长平 ,杨宁 . 无线电通信技术 . 2017,第004期
6. SpaceOS2汇编代码的形式化建模与验证方法 [C] . 周育逵 ,乔磊 ,杨桦 . 2018年第十五届全国工业控制计算机学术年会 . -1
7. 弹载软件开发中的代码自动生成与验证技术研究 [A] . 白雪峰 . 2019

汇编代码验证中的形式规范自动生成

摘要

著录项

相似文献

相关主题

期刊订阅