一句话：将 k-induction 扩展为反例引导的中间相遇双向搜索，减少发现性质违反所需步数。
k-induction 已被成功用于发现缺陷和证明正确性，但其增量执行方式在错误程序上可能浪费资源，难以快速找到性质违反。本文扩展 k-induction，利用对程序过近似所产生的反例指导搜索，将算法转化为 meet-in-the-middle 双向搜索。其主要优势是降低状态爆炸：把寻找反例所需的最大步数从 k 降至 ⌊k/2 + 1⌋，从而缩短发现性质违反所需步数。摘要未给出具体实验评估。
Recently, the k-induction algorithm has proven to be a successful approach for both finding bugs and proving correctness. However, since the algorithm is an incremental approach, it might waste resources trying to prove incorrect programs. In this paper, we extend the k-induction algorithm to shorten the number of steps required to find a property violation. We convert the algorithm into a meet-in-the-middle bidirectional search algorithm, using the counterexample produced from over-approximating the program. The main advantage is in the reduction of the state explosion by reducing the maximum required steps from k to ⌊k/2 + 1⌋.
@inproceedings{paperbot4659,
title = {Towards counterexample-guided k-induction for fast bug detection},
author = {Mikhail R. Gadelha and Felipe R. Monteiro and Lucas C. Cordeiro and Denis A. Nicole},
booktitle = {FSE},
year = {2018},
doi = {10.1145/3236024.3264840}
}