CILinear: An Automated Generation Tool of Linear Invariant
CILinear:一个线性不变式自动构造工具

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.