一句话：提出迭代器剖面这一可复用的循环不变式模板，并实现工具 LoopAnnotator 自动为基于迭代器的循环生成不变式。
演绎验证已逐步能够验证真实软件的功能正确性，但循环不变式仍需人工编写，成为主要负担。本文面向真实软件中不变式生成的两个关键需求：支持多样的索引迭代模式，以及精确刻画循环行为。作者提出迭代器剖面（iterator profile）的概念，即为某种迭代模式定义的循环不变式模板；用户为某一迭代模式编写一次剖面后，可复用于所有共享该模式的基于迭代器的循环。基于此实现了 LoopAnnotator，将迭代器剖面与对循环体的自动程序分析结果相结合来生成循环不变式。在评估中，LoopAnnotator 为先前工作基准中超过 70% 的循环成功生成不变式，并为从 Linux 内核中抽取的 245 个循环生成不变式，表明该方法能有效减轻真实代码演绎验证中的人工不变式编写负担。
Recent advances in deductive verification have gradually made it practical to verify the functional correctness of real-world software. However, creating loop invariants still requires manual effort. We propose to reduce this burden by automatically generating invariants. In the context of generating invariants for real-world software, the key requirements are to support diverse index iteration patterns and to capture precise information about loop behaviors. In this paper, we introduce the idea of an iterator profile: a loop-invariant template for an iteration pattern. Once a user writes a profile, it can be reused for any iterator-based loop that shares the same iteration pattern. We present LoopAnnotator, a tool that generates loop invariants for iterator-based loops by combining an iterator profile with the result of automatic program analysis of the loop body. LoopAnnotator successfully generates invariants for more than 70% of the loops in benchmarks from prior work and 245 loops extracted from the Linux kernel.