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

断言语言支持自定义谓词的程序验证器原型 被引量：3

Verifier Prototype for Programs with User-defined Predicates in the Assertion Language
下载PDF
导出
摘要 基于逻辑推理的方法进行程序验证是形式化程序验证的研究热点.目前的自动验证工具为了保证自动性,对描述程序性质的断言语言都有较多限制,导致程序的某些递归性质难以用断言语言表述.本文在一个面向指针程序、基于先前自行设计的形状图逻辑、依赖于自动定理证明工具Z3的自动程序验证原型系统上,通过在断言语言中引入自定义谓词来增强断言语言的表达能力,使得该原型系统不仅能自动验证含操作易变数据结构的程序的性质,也能自动验证一些不含指针的程序的性质. The automatic program verification based on logical reasoning for program properties is currently a research focus.In the automatic verification system,there are a lot of limitations on the pow er of assertion languages,therefore some recursive properties are difficult to describe.This paper presents a method to enhance the pow er of assertion language by introducing user-defined predicates.Our verifier supports properties of the programs w ith and w ithout modifiable data structures.
作者 徐文义 陈意云 李兆鹏
机构地区 中国科学技术大学计算机科学与技术学院 中国科学技术大学苏州研究院软件安全实验室
出处 《小型微型计算机系统》 CSCD 北大核心 2013年第7期1482-1486,共5页 Journal of Chinese Computer Systems
基金 国家自然科学基金项目(61003043 61170018)资助
关键词 程序验证 HOARE逻辑 形状图逻辑 程序分析 自定义谓词 software safety hoare logic user-defined predicates verification prover
分类号 TP311 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献15

  • 1Hoare C A R. An axiomatic basis for computer programming [ C ]. Communications of ACM, Oct. 1969:576-580.
  • 2Reynolds J C. Separation logic: a logic for shared mutable data structures[ C]. In Proceedings of the 17th Annual IEEE Symp. on Logic in Computer Science, Copenhagen: IEEE Computer Society Press, 2002 : 55-74.
  • 3Z Prover [ EB/OL ]. http ://research. microsoft, com/en-us/um/ redmond/projects/z3, April 2011.
  • 4The Coq Development Team. The coq proof assistant reference manual [ EB/OL ]. URL: http ://coq. inria, fr, 2009.
  • 5Liu Gang, Chen Yi-yun, Zhang Zhi-tian. Automatic inference of loop-invariant shape graphs [ J ]. Electronic Technology, 2011,38 (8): 4-6.
  • 6Li Zhao-peng. An automatic program verifier for pointerC: design and implemetation E J ]. http://ssg, ustcsz, edu. cn/ zpli/SGL/ verifier_crad, pdf, 2010.
  • 7Li Zhao-peng. A method of loop invariant inference[ EB/OLI. ht- tp://ssg, ustcsz, edu. cn/ zpli/SGL/loopinvinference cjos. pdf, Auguest 2011.
  • 8Flex[ EB/OL]. http ://flex. sourceforge, net/, May 2011.
  • 9Bison[ EB/OL]. http ://www. gnu. org/software/bison/, 2011.
  • 10Leonardo de Moura, Nikolaj Bjcmer. Z3:an efficient SMT solver [ C ]. Conference on Tools and Algorithms for the Construction and Analysis of Systems, Budapest, Hungary, LNCS ,2008,4963:337-340.

二级参考文献5

  • 1Sankaranarayanan S, Sipma H B, Manna Z Non-linear loop invariant generation using gr?bner bases[C] //Proceedings ofACM SIGPLAN Principles of Program-ming Languages(POPL'04), 2004:318-329.
  • 2Kovacs L I, Jebelean T. Finding polynomial invariants for imperative loops in the theorema system[C] //Proceedings of Verify'06, FLoC'06, 2006:52-67.
  • 3Magill S, Nanevski A, Clarke E, et al. Inferring invariants in separation logic for imperative list-processing programs [C]. Proceedings of Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE'06), January 2006.
  • 4Zhang-Y, Li Z P, Chen Y Y, et al. Shape graphlogie and shape system(extended versio-n)[EB/OL]. http://ssg.ustcsz.edu.cn/content/shape-graph-logic.Nov. 2010.
  • 5张志天 陈意云 刘刚.一个验证指针程序的方法[J].电子技术杂志,.

共引文献4

同被引文献3

引证文献3

二级引证文献2

小型微型计算机系统
2013年 第7期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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