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

计算机科学 ›› 2010, Vol. 37 ›› Issue (12): 91-95.

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

邢建英,李梦君,李舟军

(国防科技大学计算机学院长沙410073);(北京航空航天大学计算学院北京100083)

出版日期:2018-12-01 发布日期:2018-12-01
基金资助:
本文受国家自然科学基金(60703075,90718017)，国家教育部博士点基金(20070006055)资助。

CILinear: An Automated Generation Tool of Linear Invariant

XING Jian-ying,LI Meng-jun,LI Zhou-jun

Online:2018-12-01 Published:2018-12-01

摘要/Abstract

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

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

Abstract: Constructing program invariants is an important part of program verification and Interproc is an open-source tool capable of constructing linear invariant of a simple language. This paper designed and implemented a tool CILinear for automatic generation of linear invariant among numeric variables of simplified C programs based on Interproc and C compiler tool,and it is showed that CILincar can construct linear invariant effectively and deal with more syntax units.The application of CILinear in program verification was also discussed by program codes.

Key words: Linear invariant, Program verification, Numeric variable, Abstract domain, Hypergraph

邢建英,李梦君,李舟军. CILinear:一个线性不变式自动构造工具[J]. 计算机科学, 2010, 37(12): 91-95. https://doi.org/

XING Jian-ying,LI Meng-jun,LI Zhou-jun. CILinear: An Automated Generation Tool of Linear Invariant[J]. Computer Science, 2010, 37(12): 91-95. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed