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

• 作者: 李梦君 李舟军 邢建英
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 线性不变式 程序验证 数值变量 抽象域 超图
• 年，卷（期）: 2010,（12）
• 页码范围: 91-95
• 分类号: TP301
• 字数: 6543字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2010.12.020

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李舟军	北京航空航天大学计算学院	136	2221	23.0	43.0
2	李梦君	国防科技大学计算机学院	21	193	8.0	13.0
3	邢建英	国防科技大学计算机学院	3	12	2.0	3.0