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