期刊文献+

一种自适应的循环不变式生成方法 被引量:3

An Adaptive Loop Invariant Generation Approach
下载PDF
导出
摘要 基于条件赋值转换和自适应模板生成技术,提出一种自适应的的循环不变式生成方法。该方法在生成过程中综合考虑函数规范、循环本身、循环后操作等信息,有针对性地发现潜在的循环不变式,并在Frama-C平台上实现一个插件loopInv。实验结果表明,与invGen和gin-pink工具相比,loopInv的应用更加有效,可较好地完成多数程序的验证过程。 This paper proposes an improved approach to infer loop invariants which is based on conditional assignment conversion and adaptive template. Many semantic factors are considered during the generation which makes it more automatic and adaptive. A plugin named looplnv is designed and implemented. Experimental results show that the analysis is more effective, compared with other selected tools, such as invGen and gin-pink, which makes most of the procedures verified successfully.
出处 《计算机工程》 CAS CSCD 2013年第6期76-81,共6页 Computer Engineering
基金 国家自然科学基金资助项目(61170070) 国家科技支撑计划基金资助项目(2012BAK26B01) 江苏省科技支撑计划基金资助项目(BE2010032)
关键词 验证程序 循环不变式 条件赋值转换 模板 插件 verification procedures loop invariant conditional assignment conversion template plugin
  • 引文网络
  • 相关文献

参考文献18

  • 1Jung Y, Kong S, Wang B, et al.Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction[C]//Proc.of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation.Madrid, Spain: Springer, 2010.
  • 2Gopan D, Reps T W.Lookahead Widening[C]//Proc.of the 18th International Conference on Computer Aided Verification.Seattle, USA: Springer, 2006.
  • 3Bradley A R, Manna Z, Sipma H B.Linear Ranking with Reachability[C]//Proc.of the 17th International Conference on Computer Aided Verification.Edinburgh, UK: Springer, 2005.
  • 4Gulwani S, Srivastava S, Venkatesan R.Program Analysis as Constraint Solving[C]//Proc.of ACM SIGPLAN Conference on Programming Language Design and Implementation.Tucson, USA: ACM Press, 2008.
  • 5Kapur D.Automatically Generating Loop Invariants Using Quantifier Elimination[J].Deduction and Applications, 2006, 64(1): 54-75.
  • 6Monniaux D.A Quantifier Elimination Algorithm for Linear Real Arithmetic[C]//Proc.of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning.Doha, Qatar: Springer, 2008.
  • 7Bradley A R, Manna Z.Property-directed Incremental Invari- ant Generation[J].Formal Aspects of Computing, 2008, 20(4): 379-405.
  • 8Gupta A, Rybalchenko A.InvGen: An Efficient Invariant Generator[C]//Proc.of the 21th International Conference on Computer Aided Verification.Grenoble, France: Springer, 2009.
  • 9Hart T E, Ku K, Gurfinkel A, et al.Ptyasm: Software Model Checking with Proof Templates[C]//Proc.of the 23th IEEE/ ACM International Conference on Automated Software Engineering.L'Aquila, Italy: IEEE Press, 2008.
  • 10Podelski A, Rybalchenko A.A Complete Method for the Synthesis of Linear Ranking Functions[C]//Proc.of the 5th Intemational Conference on Verification, Model Checking, and Abstract Interpretation. Venice, Italy: Springer, 2004.

二级参考文献1

共引文献2

同被引文献25

引证文献3

二级引证文献4

;
使用帮助 返回顶部