一种自适应的循环不变式生成方法

doi:10.3969/j.issn.1000-3428.2013.06.015

计算机工程 ›› 2013, Vol. 39 ›› Issue (6): 76-81. doi: 10.3969/j.issn.1000-3428.2013.06.015

一种自适应的循环不变式生成方法

刘自恒^a，曾庆凯^a,b

(南京大学 a. 计算机科学与技术系；b. 计算机软件新技术国家重点实验室，南京 210093)

收稿日期:2012-04-23 出版日期:2013-06-15 发布日期:2013-06-14
作者简介:刘自恒(1987－)，男，硕士研究生，主研方向：程序分析，信息安全；曾庆凯，教授、博士生导师
基金资助:
国家自然科学基金资助项目(61170070)；国家科技支撑计划基金资助项目(2012BAK26B01)；江苏省科技支撑计划基金资助项目(BE2010032)

An Adaptive Loop Invariant Generation Approach

LIU Zi-heng ^a, ZENG Qing-kai^a,b

(a. Department of Computer Science and Technology; b. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China)

Received:2012-04-23 Online:2013-06-15 Published:2013-06-14

摘要/Abstract

摘要： 基于条件赋值转换和自适应模板生成技术，提出一种自适应的的循环不变式生成方法。该方法在生成过程中综合考虑函数规范、循环本身、循环后操作等信息，有针对性地发现潜在的循环不变式，并在Frama-C平台上实现一个插件loopInv。实验结果表明，与invGen和gin-pink工具相比，loopInv的应用更加有效，可较好地完成多数程序的验证过程。

关键词: 验证程序, 循环不变式, 条件赋值转换, 模板, 插件

Abstract: 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 loopInv 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.

Key words: verification procedure, loop invariant, conditional assignment conversion, template, plugin

中图分类号:

TP311

刘自恒, 曾庆凯. 一种自适应的循环不变式生成方法[J]. 计算机工程, 2013, 39(6): 76-81.

LIU Zi-Heng, CENG Qiang-Kai. An Adaptive Loop Invariant Generation Approach[J]. Computer Engineering, 2013, 39(6): 76-81.

http://www.ecice06.com/CN/Y2013/V39/I6/76

参考文献

[1] Jung 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.
[2] Gopan D, Reps T W. Lookahead Widening[C]//Proc. of the 18th International Conference on Computer Aided Verification. Seattle, USA: Springer, 2006.
[3] Bradley 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.
[4] Gulwani 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.
[5] Kapur D. Automatically Generating Loop Invariants Using Quantifier Elimination[J]. Deduction and Applications, 2006, 64(1): 54-75.
[6] Monniaux 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.
[7] Bradley A R, Manna Z. Property-directed Incremental Invari- ant Generation[J]. Formal Aspects of Computing, 2008, 20(4): 379-405.
[8] Gupta A, Rybalchenko A. InvGen: An Efficient Invariant Generator[C]//Proc. of the 21th International Conference on Computer Aided Verification. Grenoble, France: Springer, 2009.
[9] Hart 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.
[10] Podelski A, Rybalchenko A. A Complete Method for the Synthesis of Linear Ranking Functions[C]//Proc. of the 5th
International Conference on Verification, Model Checking, and Abstract Interpretation. Venice, Italy: Springer, 2004.
[11] Lalire G, Argoud M, Jeannet B. Interproc[EB/OL]. (2008-10- 21). http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/ interproc/index.html.
[12] Moy Y, Marché C. Modular Inference of Subprogram Contracts for Safety Checking[J]. Journal of Symbolic Computation, 2010, 45(11): 1184-1211.
[13] 邢建英, 李梦君, 李舟军. CILinear: 一个线性不变式自动构造工具[J]. 计算机科学, 2010, 37(12): 91-95.
[14] Jung Y, Kong S, David C, et al. Automatically Inferring Loop Invariants via Algorithmic Learning[C]//Proc. of MSCS’12. [S. 1.]: IEEE Press, 2012.
[15] Ernst M D, Perkins J H, Guo P J, et al. The Daikon System for Dynamic Detection of Likely Invariants[J]. Science of Computer Programming, 2007, 69(1-3): 35-45.
[16] Furia C A, Meyer B. Inferring Loop Invariants Using Post- conditions[M]. Berlin, Germany: Springer [s. n.], 2010.
[17] Sharma R, Dillig I, Dillig T, et al. Simplifying Loop Invariant Generation Using Splitter Predicates[C]//Proc. of the 23th International Conference on Computer Aided Verification. Cliff Lodge, USA: Springer, 2011.
[18] Kovács L, Voronkov A. Finding Loop Invariants for Programs over Arrays Using a Theorem Prover[C]//Proc. of the 12th International Conference on Fundamental Approaches to Software Engineering. York, UK: Springer, 2009.
编辑索书志
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

选择文件类型/文献管理软件名称

选择包含的内容

一种自适应的循环不变式生成方法

An Adaptive Loop Invariant Generation Approach

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

[1]	李博, 黄东强, 贾金芳, 吴利, 王晓英, 黄建强. 基于CPU与GPU的异构模板计算优化研究[J]. 计算机工程, 2023, 49(4): 131-137.
[2]	安志国, 彭政, 易满成, 刘健欣, 俞思帆. 神经网络滤波器竞争训练[J]. 计算机工程, 2023, 49(4): 120-124.
[3]	任立成, 杨嘉棋, 魏宇星, 张建林. 基于特征融合与双模板嵌套更新的孪生网络跟踪算法[J]. 计算机工程, 2021, 47(7): 239-248.
[4]	孙家异, 韦永壮. 轻量级分组密码算法DoT的模板攻击[J]. 计算机工程, 2021, 47(3): 155-159,165.
[5]	尚桠朝, 孟令军. 基于多特征和尺度估计的KCF_MTSA算法[J]. 计算机工程, 2021, 47(3): 102-108,116.
[6]	程希希, 张艳玲, 田军委. 基于模板匹配的快速角点检测方法[J]. 计算机工程, 2020, 46(7): 222-227.
[7]	程志炜, 陈财森, 朱连军, 莫伟锋, 王会宇. 基于Pearson相关系数的Cache计时模板攻击方法[J]. 计算机工程, 2019, 45(7): 159-163.
[8]	陈威,李决龙,邢建春,杨启亮,周启臻. 融合前景信息的背景模板优化显著性检测算法[J]. 计算机工程, 2019, 45(1): 221-225,232.
[9]	高峰,刘震,高辉. 结合有监督广度优先搜索策略的通用垂直爬虫方法[J]. 计算机工程, 2018, 44(11): 289-299.
[10]	刘旭亮,钟浩. 一种基于StackOverflow分析的程序自动修复方法[J]. 计算机工程, 2018, 44(10): 95-100.
[11]	周军娜,陈伟,王珂,蔡长征. 基于TLD的稀疏原型目标跟踪算法[J]. 计算机工程, 2017, 43(6): 236-240.
[12]	邹冲,蔡敦波,赵娜,刘莹,赵彤洲. 基于SVM-LeNet模型融合的行人检测算法[J]. 计算机工程, 2017, 43(5): 169-173.
[13]	聂进焱,魏艳涛,瞿少成. 一种面向局部神经反应的模板选取算法[J]. 计算机工程, 2017, 43(3): 277-281.
[14]	陈树,杨天. 一种基于改进ZS细化算法的指针仪表检测[J]. 计算机工程, 2017, 43(12): 216-221.
[15]	刘冠群,罗桂琼,谭平. 基于类Haar特征模板匹配的多镜头步态识别算法[J]. 计算机工程, 2017, 43(12): 231-236.

模态框（Modal）标题

选择文件类型/文献管理软件名称

选择包含的内容

一种自适应的循环不变式生成方法

An Adaptive Loop Invariant Generation Approach

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价