期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

CILinear:一个线性不变式自动构造工具 被引量：3

CILinear:An Automated Generation Tool of Linear Invariant
下载PDF
导出
摘要 构造不变式是程序验证的重要组成部分,而开源工具Interproc能对简单的程序设计语言构造线性不变式。基于Interproc和C程序编译工具CIL,针对简化的C程序设计并实现了自动构造数值型程序变量线性不变式的工具CILinear,并与Interproc进行了比较。实验表明CILinear能有效地构造线性不变式,并且比Interproc支持的语法更多。通过实例讨论了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 CILinear can construct linear invariant effectively and deal with more syntax units.The application of CILinear in program verification was also discussed by program codes.
作者 邢建英 李梦君 李舟军
机构地区 国防科技大学计算机学院 北京航空航天大学计算学院
出处 《计算机科学》 CSCD 北大核心 2010年第12期91-95,共5页 Computer Science
基金 国家自然科学基金(60703075 90718017) 国家教育部博士点基金(20070006055)资助
关键词 线性不变式 程序验证 数值变量 抽象域 超图 Linear invariant Program verification Numeric variable Abstract domain Hypergraph
分类号 TP301 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献1

二级参考文献46

  • 1Cousot P, Cousot R. Systematic design of program analysis frameworks. In: Proc. of the 6th POPL. San Antonio: ACM Press, 1979. 69-282. http://www.di.ens.fr/-cousot/COUSOTpapers/POPL79.shtml
  • 2Cousot P, Cousot R. Abstract interpretation frameworks. Journal of Logic and Computer, 1992,2(4):511-547.
  • 3Cousot P, Cousot R. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe M, Wirsing M, eds. Proc. of the PLILP'92. LNCS 631, Springer-Verlag, 1992. 269-295.
  • 4Cousot P. Abstract interpretation based formal methods and future chanllenges. In: Wilhelm R, ed. Informatics——10 Years Back, 10 Years Ahead. Berlin, Heidelberg: Springer-Verlag, 2000. 138-156.
  • 5Cousot P, Cousot R. Abstract interpretation based program testing. In: Proc. of the SSGRR 2000 Computer & eBusiness Int'l Conf. 2000. Compact disk paper 248. http://www.di.ens.fr/-cousot/COUSOTpapers/SSGRRP-00-PC-RC.shtml
  • 6Cousot P, Cousot R. Basic concepts of abstract interpretation. In: René J, ed. Building the Information Society. Toulouse: Kluwer Academic Publishers, 2004. 359-366.
  • 7Cousot P, Cousot R. Refining model checking by abstract interpretation. Automated Software Engineering Journal (Special Issue on Automated Software Analysis), 1999,6(1):69-95.
  • 8Cousot P, Cousot R. Static determination of dynamic properties of programs. In: Robinet B, ed. Proc. of the 2nd Int'l Symp. on Programming. Paris, 1976. 106-130. http://www.di.ens.fr/-cousot/COUSOTpapers/ISOP76.shtml
  • 9Cousot P, Halbwachs N. Automatic discovery of linear restraints among variables of a program. In: Proc. of the 5th POPL. Arizona: ACM Press, 1978. 84-97.
  • 10Miné A. The octagon abstract domain. Higher-Order and Symbolic Computation, 2006,19(1):31-100.

共引文献29

同被引文献35

  • 1Floyd R W. Assigning meanings to programs[ C]//Proc. of a Symposium on Applied Mathematics. NewYork, 1967,19 : 19-31.
  • 2Hoare C A R. An axiomatic basis for computer programming [ J]. Comm. ACM, 1969,12(10) :576-580.
  • 3GaS1 Lalire, Mathias Argoud, Bertrand Jeannet. Interproc [ EB/OL]. http ://pop-art. inrialpes, fr/-bjeannet/bjean- net-forge/interproc/index, html, 2008-014)1.
  • 4Bertrand Jeannet, Antoine Mine. The APRON Library for Numerical Abstract Domains [ EB/OL]. http ://apron. cri. ensmp, fr/library/ ,2011-04-07.
  • 5Laura Kov6cs. Aligator: A mathematica package for invari- ant generation ( system description ) [ C ]//IJCAR' 08. 2008 : 275-282.
  • 6Wolfram S. The Mathematica Book(Version 5. O) [ M]. Wolf- ram Media,2003.
  • 7Buchberger B, Craciun A,Jebelean T,et al. Theorema :Towards computer-aided mathematical theory exploration[ J ]. Journal of Applied Logic ,2006,4(4) :470-504.
  • 8Xing Jianying, Li Mengjun, Li Zhoujun. Automated program verification using generation of invariants [ C ]//QSIC. 2010 : 300 -305.
  • 9Collins G E. Quantifier elimination for real closed fields by cylindrical algebraic decomposition [ C ]//GI Conf. Automata Theory and Formal Languages. 1975:515-532.
  • 10Sumit Gulwani. SPEED:Symbolic complexity bound analysis [ C ]//CAV 2009. 2009:51-62.

引证文献3

二级引证文献5

计算机科学
2010年 第12期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部