基于克雷格插值的反例理解方法

针对错误原因提取效率低的问题,提出一种利用克雷格插值对模型检测器产生的反例进行自动理解的方法.该方法首先从反例失效状态出发推导出其最弱前置条件,然后对初始状态与反例最弱前置条件进行不一致分析,能在线性时间内提取克雷格插值作为反例失效原因,产生的插值能直接用于定位错误事件.实验结果表明,基于克雷格插值的反例理解方法能显著提高反例理解速度,提高软件的调试效率,从而提升软件的可靠性和质量.