主页 / 安全论文每日读 / Combining Symbolic Execution and Model Checking for Data Flow Testing
  • 作者
    GoSSIP @ LoCCS.Shanghai Jiao Tong University
  • 简介

    Combining Symbolic Execution and Model Checking for Data Flow Testing 是一篇发表在ICSE‘15会议上的论文 。本文提出了通过符号执行和模型测试以提高动态数据流分析代码覆盖率的方法。

    Overview

    • Data Flow Testing(DFT)的目的是通过观察程序中变量所有被使用的情况以证明其被使用正确
    • 问题:
      • 现存的 data flow coverage 工具很少,已知的只有20年前的ATAC
      • 数据流的test data的生成复杂度高;要生成覆盖变量定义、使用的测试用例比只覆盖程序语句要复杂 (路径爆炸)
      • 不可达的测试目标使得DFT更加困难
    • 方法:
      • Dynamic Symbolic Execution (DSE)
      • Counter example-Guided Abstraction Refinement(CEGAR)
        • 给定源码和假设,静态分析证明程序满足假设、或者给出反例
  • 援引
    http://www.securitygossip.com/blog/2016/04/08/2016-04-08/
  • 提示
    本站仅做资料的整理和索引,转载引用请注明出处
相关推荐
附件下载
  • Combining.Symbolic.Execution.and.Model.Checking.for.Data.Flow.Testing阅读笔记.pdf
    时间: 大小: 0.2 M 下载: 39
  • Combining.Symbolic.Execution.and.Model.Checking.for.Data.Flow.Testing.pdf
    时间: 大小: 0.89 M 下载: 14