A Program Instrumentation Framework for Automatic Verification
Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer, Marten Voorberg
TL;DR
The paper tackles the gap between expressive specifications and back-end verification tools by introducing program instrumentation as a formal, automatic framework that rewrites programs to eliminate hard constructs while preserving correctness. It formalizes an instrumentation operator (G,R,I), along with an automated application strategy, enabling automatic discovery of instrumented programs whose verification implies the original program’s correctness. Using a monoid-homomorphism-based approach, the authors develop operators for quantification over arrays and for aggregations, including non-cancellative and cancellative monoids, and provide soundness and (relative) completeness results. The Mono-Cera tool demonstrates practical impact by automatically verifying a significant set of SV-COMP programs involving array quantification and aggregation, outperforming several existing fully automatic back-ends on challenging benchmarks. This framework promises scalable verification for complex array properties and supports back-translation of witnesses and counterexamples, with future work aimed at expanding the operator library and applying the approach to broader data-structures and arithmetic forms.
Abstract
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.