这篇paper的完整题目是 Feedback-Driven Dynamic Invariant Discovery
Motivation
- 之前的工具找 specification 有一些问题
- 获得错误的、不精确的 specification
- 漏掉了本应有的 specification
- 为了改进 specification，Daicon 需要优质的测试集，但是目前的技术难以获得
1、Intro
- 用 Daicon 生成的 invariant 来合成 assertion
- 这些 assertion 被 instrument 到程序里
- 可以减少坏 specification，增加好 specification
- 对新的程序进行符号执行，获得新的测试集
- 循环这个 loop，达到一个定点停止
- 定点：推断的 invariant 不再变化
- 变化的原因：新的测试例违背了之前的 assertion
- assertion separation（？）
- violation restriction（？）
- 对符号执行的过程进行剪枝
- 简化 PC
- 约束求解复用
2、例程
- 初始 Daicon 生成了7个 invariants
- 经过3次 iteration 后，选出了3个好的，剔除了4个不精确的
3、实现
- 对于每个 assertion，符号执行都试图访问 false 的那个 branch
- 用现成的约束求解器求解，生成新的测试例
- iDiscovery 未必能找到所有的 invariant
- 复杂度：iDiscovery 增加了 m 个 assertion，那么就会增加 m 个 PC
- 优化算法：看不懂
5、实验
- 只需4个 iteration 就能显著减少 invariant 的数量
- 应用两种优化方法可以
- 显著减少 iteration 的数量，从而减少运行时间
- 可能会减少 invariant 的数量
