CILinear:一个线性不变式自动构造工具

邢建英; 李梦君; 李舟军

首页> 中文期刊>计算机科学 >CILinear:一个线性不变式自动构造工具

CILinear:一个线性不变式自动构造工具

开具论文收录证明 >>

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

页面导航

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

摘要

构造不变式是程序验证的重要组成部分,而开源工具Interproc能对简单的程序设计语言构造线性不变式.基于Interproc和C程序编译工具CIL,针对简化的C程序设计并实现了自动构造数值型程序变量线性不变式的工具CILinear,并与Interproc进行了比较.实验表明CILinear能有效地构造线性不变式,并且比Interproc支持的语法更多.通过实例讨论了CILinear在程序验证中的实际应用.

著录项

来源
《计算机科学》|2010年第12期|91-95|共5页
作者
邢建英; 李梦君; 李舟军;
展开▼
作者单位

国防科技大学计算机学院,长沙,410073;

国防科技大学计算机学院,长沙,410073;

北京航空航天大学计算学院,北京,100083;

展开▼
原文格式 PDF
正文语种 chi
中图分类理论、方法;
关键词
线性不变式; 程序验证; 数值变量; 抽象域; 超图;
入库时间 2022-08-18 04:38:30

相似文献

中文文献
外文文献
专利

1. 非线性循环不变式的自动生成 [J] . 毕忠勤 ,曾振柄 ,郭远华 . 计算机应用 . 2008,第007期
2. 一个用于构造非线性半定规划算法的非线性Lagrange函数 [J] . 李阳 ,王一伊 . 大连民族学院学报 . 2010,第003期
3. 构造反例的一个有力工具——Dirichlet函数 [J] . 胡绍宗 . 高等数学研究 . 2015,第004期
4. 一个本体语言及本体构造工具的设计 [J] . 徐立广 ,金芝 ,易利军 . 计算机工程与应用 . 2006,第025期
5. 一个构造和操作决策表的工具—PROLOGA [J] . 李思源 . 计算机工程与应用 . 1997,第004期
6. 构造一个可靠高效稳健的水调自动化系统——三峡梯级水调自动化系统建设经验浅谈 [C] . 刘宇 ,周保红 . 中国南方十三省（市、区）水电学会联络会暨学术交流研讨会 . 2006
7. 循环不变式自动探测 [A] . 黄小明 . 2017

CILinear:一个线性不变式自动构造工具

摘要

著录项

相似文献

相关主题

期刊订阅