Dec, 2017
用角-ICE学习方法合成不变量和契约
Horn-ICE Learning for Synthesizing Invariants and Contracts
TL;DR本研究基于Horn implication counterexamples (Horn-ICE)设计了学习算法，提出了一种决策树学习算法，可以从Horn-ICE样本中学习并在多项式时间内工作。使用统计启发式学习小树的方法，以满足样本。实验结果表明，我们算法的实现可以高效地为各种顺序和并发程序学习充分的归纳式不变量和契约。