%0 Journal Article
%T CILinear: An Automated Generation Tool of Linear Invariant<br>CILinear:一个线性不变式自动构造工具
%A XING Jian-ying
%A LI Meng-jun
%A LI Zhou-jun
%A <br>邢建英
%A 李梦君
%A 李舟军
%J 计算机科学
%D 2010
%I 
%X 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.
%K Linear invariant
%K Program verification
%K Numeric variable
%K Abstract domain
%K Hypergraph<br>线性不变式，程序验证，数值变量，抽象域，超图
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=45DE4E3054D47994804E1D944C9805B5&yid=140ECF96957D60B2&vid=42425781F0B1C26E&iid=59906B3B2830C2C5&sid=C753EB8AC8F551B9&eid=C36EC077A8A90308&journal_id=1002-137X&journal_name=计算机科学&referenced_num=1&reference_num=0