• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >Automating Program Verification and Repair Using Invariant Analysis and Test Input Generation.
【24h】

Automating Program Verification and Repair Using Invariant Analysis and Test Input Generation.

机译：使用不变分析和测试输入生成来自动进行程序验证和修复。

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Software bugs are a persistent feature of daily life---crashing web browsers, allowing cyberattacks, and distorting the results of scientific computations. One approach to improving software uses program invariants---mathematical descriptions of program behaviors---to verify code and detect bugs. Current invariant generation techniques lack support for complex yet important forms of invariants, such as general polynomial relations and properties of arrays. As a result, we lack the ability to conduct precise analysis of programs that use this common data structure. This dissertation presents DIG, a static and dynamic analysis framework for discovering several useful classes of program invariants, including (i) nonlinear polynomial relations, which are fundamental to many scientific applications; disjunctive invariants, (ii) which express branching behaviors in programs; and (iii) properties about multidimensional arrays, which appear in many practical applications. We describe theoretical and empirical results showing that DIG can efficiently and accurately find many important invariants in real-world uses, e.g., polynomial properties in numerical algorithms and array relations in a full AES encryption implementation.;Automatic program verification and synthesis are long-standing problems in computer science. However, there has been a lot of work on program verification and less so on program synthesis. Consequently, important synthesis tasks, e.g., generating program repairs, remain difficult and time-consuming. This dissertation proves that certain formulations of verification and synthesis are equivalent, allowing for direct applications of techniques and tools between these two research areas. Based on these ideas, we develop CETI, a tool that leverages existing verification techniques and tools for automatic program repair. Experimental results show that CETI can have higher success rates than many other standard program repair methods.
机译：软件错误是日常生活的一个持久特征-导致网络浏览器崩溃，允许网络攻击并扭曲科学计算的结果。一种改进软件的方法是使用程序不变式（程序行为的数学描述）来验证代码并检测错误。当前的不变式生成技术缺乏对复杂但重要形式的不变式的支持，例如一般的多项式关系和数组的性质。结果，我们缺乏对使用此通用数据结构的程序进行精确分析的能力。本文提出了一种DIG模型，它是一种静态和动态的分析框架，可用于发现几种有用的程序不变式类型，其中包括：（i）非线性多项式关系，这对许多科学应用都是至关重要的；析取不变量，（ii）表示程序中的分支行为； （iii）有关多维数组的属性，这些属性出现在许多实际应用中。我们描述的理论和经验结果表明，DIG可以在实际应用中高效，准确地找到许多重要的不变量，例如，数值算法中的多项式特性和完整AES加密实现中的数组关系。计算机科学中的问题。但是，关于程序验证的工作很多，而关于程序综合的工作却很少。因此，重要的综合任务，例如产生程序修复，仍然困难且耗时。本文证明了验证和综合的某些公式是等效的，从而允许在这两个研究领域之间直接应用技术和工具。基于这些想法，我们开发了CETI，这是一种利用现有验证技术和工具进行自动程序修复的工具。实验结果表明，CETI可以比许多其他标准程序修复方法具有更高的成功率。

著录项

  • 作者

    Nguyen, ThanhVu Huy.;

  • 作者单位

    The University of New Mexico.;

  • 授予单位 The University of New Mexico.;
  • 学科 Computer science.
  • 学位 Ph.D.
  • 年度 2014
  • 页码 176 p.
  • 总页数 176
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号