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 its correctness instead. In this paper, we propose 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 formalise array aggregation operations as monoid homomorphisms. 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程序）上进行了评估。