In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about this equivalent program instead. In this article, we propose program instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.

翻译：在演绎验证与软件模型检查中，当后端求解器能力不足或缺乏所需理论时，处理某些规约语言结构可能存在问题。一种应对方法是为验证目的，将程序转换为不使用问题结构的等价程序，并转而推理该等价程序。本文提出程序插装作为一种统一的验证范式，该范式可涵盖多种现有特设方法，具有明确的形式化正确性标准，能够自动应用，并可回传证据与反例。我们通过涉及数组上量化与聚合操作（例如数组给定区间的元素最大值或总和）的自动化程序验证来阐述本方法，这类操作已知难以进行自动推理。我们在专为聚合程序验证设计的MonoCera工具中实现了本方法，并在示例程序（包括SV-COMP程序）上进行了评估。