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.

The effort of formal verification of large heterogeneous systems needs to scale linearly with the number of interacting components, to be feasible in industrial practice. This is made possible by compositional specification methods and proof systems. In this paper, we demonstrate how trustworthy verified decomposition can be performed for an industry-relevant embedded system: a fuel level display. We first formalize the underlying theory in the HOL4 theorem prover, and augment this theory to allow specifications using Metric Interval Temporal Logic (MITL). We then state a top-level specification for our system using MITL and decompose it down to the system components. Our HOL4 formalization provides a corrected and extended restatement of a general specification language and proof system from previous work and showcases its usefulness for verified decomposition of systems.

Traditionally, programs are formally specified and verified with respect to their computational domain, disregarding the domain in which they are to be applied. This, however, is inadequate for programs that simulate processes in a specific application domain, or programs that generate data that must conform to external, domain-specific specifications. Such programs need also to be correct with respect to their application domain. This work presents a Hoare Logic that manages two different perspectives on a program during a correctness proof: the computational view and the domain view. This enables us to specify the correctness of a program in terms of the domain without referring to the computational details, but at the same time to interpret failed proof attempts in the domain. For domain specification, we illustrate the use of description logics and base our approach on semantic lifting, an approach to interpret a program as a knowledge graph. We present a calculus that uses translations between both kinds of assertions, thus separating the concerns in specification, but enabling the use of description logic in verification.

We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed points, for precise specification of programs with recursive procedures. Both programs and trace formulas are equipped with a direct-style, fully compositional, denotational semantics that on programs coincides with the standard SOS of recursive programs. We design a compositional proof calculus for proving finite-trace program properties, and prove soundness as well as (relative) completeness. We show that each program can be mapped to a semantics-preserving trace formula and, vice versa, each trace formula can be mapped to a canonical program over slightly extended programs, resulting in a Galois connection between programs and formulas. Our results shed light on the correspondence between programming constructs and logical connectives.

Model checking temporal properties of software is algorithmically hard. To be practically feasible, it usually requires the creation of simpler, abstract models of the software, over which the properties are checked. However, creating suitable abstractions is another difficult problem. We argue that such abstract models can be obtained with little effort, when the state transformation properties of the software components have already been deductively verified. As a concrete, language-independent representation of such abstractions we propose the use of flow graphs, a formalism previously developed for the purposes of compositional model checking. In this paper, we describe how we envisage the work flow and tool chain to support the proposed verification approach in the context of embedded, safety-critical software written in C.

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.

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.

In embedded systems development, contract based design is a design paradigm where a system is divided hierarchically into components and developed in a top-down manner, using contracts as a means to divide responsibilities and manage the complexity of the system. Contract theories provide a formal basis for reasoning about the properties of the system, and of the contracts themselves. In previous work, we have developed a contract theory for sequential, procedural programs, that is defined abstractly, at the semantic level. The theory fulfils well-established, desired properties of system design. In this paper, we present a methodology for applying the contract theory in real embedded software design. We show how to instantiate the contract theory with concrete syntaxes for defining components and contracts, and how the contract theory enables formal reasoning about the resulting objects. In order to cope with the need for different behavioural models at different levels of abstraction in an embedded system, we extend the contract theory through parametrisation on the semantic domain. We illustrate the application of the proposed methodology on a small, but realistic example, where the temporal logic TLA is used for reasoning at the system level, while lower level components are specified using pre- and post-conditions in the form of ACSL, a specification language for C.

Contracts specifying a procedure’s behavior in terms of pre- and postconditions are essential for scalable software verification, but cannot express any constraints on the events occurring during execution of the procedure. This necessitates to annotate code with intermediate assertions, preventing full specification abstraction. We propose a logic over symbolic traces able to specify recursive procedures in a modular manner that refers to specified programs only in terms of events. We also provide a deduction system based on symbolic execution and induction that we prove to be sound relative to a trace semantics. Our work generalizes contract-based to trace-based deductive verification by extending the notion of state-based contracts to trace-based contracts.