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

基于抽象解释的函数不变量正确性验证

Abstract Interpretation Based Correct Verification for Functional Invariant
下载PDF
导出
摘要 函数不变量检测是提高软件质量的一种有效方法.针对检测方法可能带来无效的函数不变量的缺陷,提出一种以抽象解释理论为基础的函数不变量的正确性验证方法.首先将函数不变量转化成多项式关系;其次结合多项式程序与最弱前置条件抽象解释分析多项式关系正确性的判断依据;最后构造多项式关系算法,凭借得到的结果验证函数不变量正确与否.同时通过一个C程序中的函数不变量为例对该验证方法进行说明. The discovery of function invariant is an effective method for improving software quality. As the detecting may contain invalid invariant defects, this paper proposes an abstract interpretation based correct verification for functional invariant. Firstly functional invariants transfer foundation of the correctness of polynomial relations with to polynomial relations. Secondly we abstract analysis the polynomial program and the weakest precondition. Finally we construct polynomial algorithm and verify the function invariant is correct or not with the results obtained. As the same time we state this verification with functional invariant of an C program.
作者 武书彦 苏青琴 刘久富
机构地区 郑州牧业工程高等专科学校信息工程系 南京航空航天大学自动化学院
出处 《微电子学与计算机》 CSCD 北大核心 2012年第10期161-165,共5页 Microelectronics & Computer
基金 国家自然科学基金项目(60674100)
关键词 函数不变量 抽象解释 正确性验证 多项式关系 functional invariant abstract interpretation correct verification~ polynomial relations
分类号 TP311 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献5

  • 1Ernst M D. static and dynamic analysis: synergy and duality[C] // WODA 2003: ICSE workshop on Dy- namic Analysis. Portland: ICSE, 2003 : 24-27.
  • 2Cousot P,Cousot tL Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[C]//Proc of the 4th POPL. Los Angeles: ACM Press, 1977: 238- 252.
  • 3李梦君,李舟军,陈火旺.基于抽象解释理论的程序验证技术[J].软件学报,2008,19(1):17-26. 被引量：30
  • 4Cousot P,Cousot R. Abstract interpretation..A unified lattice model for static analysis of programs by con- struction or approximation of fixpoints[C]//Proc of the 4th POPL. Los Angeles.-ACM Press, 1977: 238: 252.
  • 5Cousot P, CousotTo Abstract interpretation based program testing[C]//Proceedings of the SSGRR 2000 Computer&Business Conference. L'Aquila, Italy IEEE: 2000.

二级参考文献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

微电子学与计算机
2012年 第10期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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