一句话：提出区间反例以提升循环不变式黑盒学习中的样例质量，减少约束查询次数。
循环不变式生成是程序验证中的长期难题。近年来，黑盒学习作为推断循环不变式的一种有前景的方法受到关注，然而其性能严重依赖于所收集样例的质量。在许多情况下，必须经过数十次甚至数百次约束查询才能成功推断出可行的不变量。本文提出区间反例（interval counterexamples）以改进样例质量，旨在减少约束查询次数，提升循环不变式学习的效率。
Loop invariant generation has long been a challenging problem. Black-box learning has recently emerged as a promising method for inferring loop invariants. However, the performance depends heavily on the quality of collected examples. In many cases, only after tens or even hundreds of constraint queries, can a feasible invariant be successfully inferred.
DOI 原文 ·
@inproceedings{paperbot5729,
title = {Interval counterexamples for loop invariant learning},
author = {Rongchen Xu and Fei He and Bow-Yaw Wang},
booktitle = {FSE},
year = {2020},
doi = {10.1145/3368089.3409752}
}