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

摘要：

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

关键词：线性不变式、程序验证、数值变量、抽象域、超图

所属期刊栏目：37

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金60703075,90718017;国家教育部博士点基金20070006055

在线出版日期：2011-03-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：91-95