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.

In this paper, we report on our experience with formally specifying and verifying an industrial software module, provided to us by a company from the heavy-vehicle industry. We start with a set of 32 informally stated requirements, also provided by the company. We discuss at length the formalization process of informally stated requirements for the purposes of their subsequent formal verification. Depending on the nature of each requirement, one of three languages was used: ACSL contracts, LTL or MITL. We use the Frama-C deductive verification framework to verify the source code of the module against the formalized requirements, with the outcome that 21 requirements are successfully verified while 6 are not. The remaining 5 requirements could not be verified for the module itself, as they specify behavior outside it. We illustrate what steps we took to convert LTL and MITL formulas into ACSL contracts to enable their verification in Frama-C. Finally, we discuss conclusions we drew from our work, notably that formal-verification-driven development of modules and verified breakdown of system requirements could likely remedy some problems we encountered.

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 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 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.