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