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

命令式程序终止性验证方法综述

Overview of termination verification methods for imperative programs
下载PDF
导出
摘要 作为软件完全正确性的重要组成部分,程序终止性受到越来越多的关注。旨在跟踪国内外针对命令式程序的终止性验证方法,调研该领域的最新研究成果,同时提出解决该问题的建议性方法框架,对命令式程序终止性研究提供有意义的帮助。给出了程序终止性问题的定义,介绍了已有的数值程序、堆操作程序终止性验证方法,并分别进行了分析与对比。总结了当前研究中存在的难点与热点问题,给出了一种基于模型检验的C程序终止性验证框架,该框架可以作为研究命令式程序终止性的基本框架。 As an important integral part of the full correctness of software, termination property ot programs has gameo more and more attention.This paper tries to investigate the termination verification methods for imperative programs both at home and abroad, and concludes the newest research results.A suggestion solution for this problem is also presented, which is helpful for future researches.The problem of program termination is defined.Existing termination verification methods for numeric programs and heap manipulating programs are introduced and compared separately.The hard problems and hot toPics are also concluded and presented.A termination verification framework for C programs is presented and that can work as a starting framework for researching the termination property of imperative programs.
作者 李仁见 王昭飞
机构地区 国防科技大学计算机学院并行与分布处理国家重点实验室
出处 《计算机工程与应用》 CSCD 北大核心 2011年第28期1-6,105,共7页 Computer Engineering and Applications
基金 国家自然科学基金(No.60725206) 国家973项目课题(No.2011CB302603)~~
关键词 终止性 命令式程序 秩函数 尺寸变化终止(SCT)分析 模型检验 termination imperative program ranking function Size-Change Termination（SCT） analysis model checking
分类号 TP311 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献37

  • 1Cook B, Podelski A, Rybalchenko A.Terminafion proofs for systems code[C]//Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation (PLDI), Ottawa, Ontario, Canada, 2006: 415-426.
  • 2Cook B, Gotsman A, Podelski A, et al.Proving that programs eventually do something good[C]//POPL,2007:265,276.
  • 3Tiwari A.Termination of linear programs[C]//LNCS 3114: Computer Aided Verification(CAV) ,2004:70-82.
  • 4Parameswaran A G.Discovering termination and invariant generation[R].Bombay Mumbai:Department of Computer Science and Engineering Indian Institute of Technology, 2006.
  • 5Cousot EProving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming[C]//VMCAI, 2005:1-24.
  • 6Bradley A R, Manna Z, Sipma H B.Termination of polynomial programs[C]//VMCAI, 2005:113 - 129.
  • 7Yang Lu,Zhan Naijun,Xia Bican, et al.Program verification by using DISCOVERER[C]/NSTTE, 2005: 528-538.
  • 8姚勇.区间上非线性程序的终止性判定[J].软件学报,2010,21(12):3116-3123. 被引量：8
  • 9Dams D, Gerth R, Grumberg O.A heuristic for the automatic generation of ranking functions[C]//Workshop on Advances in Verification, 2000:1-8.
  • 10ColSn M, Sipma H.Synthesis of linear ranking functions[C]// TACAS, 2001:67-81.

二级参考文献15

  • 1Podelski A, Rybalchenko A. A complete method for the synthesis of linear ranking functions. In: Steffen B, ed. Proc. of the Verification, Model Checking, and Abstract Interpretation. LNCS 2937, Heidelberg: Springer-Verlag, 2004. 239-251.
  • 2Dams D, Gerth R, Grumberg O. A heuristic for the automatic generation of ranking functions. In: Alur R, ed. Proc. of the Workshop on Advances in Verification. Chicago: University of Utah Press, 2000. 1-8.
  • 3Colon M, Sipma HB. Synthesis of linear ranking functions. In: Margaria T, ed. Proc. of the Tools and Algorithms for Construction and Analysis of Systems. LNCS 2031, Heidelberg: Springer-Verlag, 2001.67-81.
  • 4Chen YH, Xia BC, Yang L, Zhan N J, Zhou CC. Discovering non-linear ranking functions by solving semi-algebraic systems. In: John F, ed. Proe. of the Theoretical Aspects of Computing (ICTAC 2007). Heidelberg: Springer-Verlag, 2007.34-49.
  • 5Tiwari A. Termination of linear programs. In: Alur R, ed. Proc. of the Computer Aided Verification. LNCS 3114, Heidelberg: Springer-Verlag, 2004. 70-82.
  • 6Cousot P. Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semi-definite programming. In: Cousot R, ed. Proc. of the Verification, Model Checking, and Abstract Interpretation. LNCS 3385, Heidelberg: Springer-Verlag, 2005.61-81.
  • 7Bradley AR, Manna Z, Sipma HB. Termination of polynomial programs. In: Cousot R, ed. Proc. of the Verification, Model Checking, and Abstract Interpretation. LNCS 3385, Heidelberg: Springer-Verlag, 2005. 113-129.
  • 8Yang L, Zhan NJ, Xia BC, Zhou CC. Program verification by using DISCOVERER. In: Meyer B, ed. Proc. of the Verified Software. LNCS 4171, Heidelberg: Springer-Verlag, 2008. 528-538.
  • 9Li T, Yorke JA. Period three implies chaos. American Mathematical Monthly, 1975,82(10):985-992. [do/: 10.2307/2318254].
  • 10Zhang JZ, Yang L. Some theorems on Sarkovskii order. Advances in Mathematics, 1987,16(1):33-48 .

共引文献7

计算机工程与应用
2011年 第28期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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