Information Exchange in Software Verification

Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The analysis is necessarily an over-approximation as the real executions of the program are not available at analysis time. In contrast, runtime verification techniques have been extensively used for control-oriented properties, analysing the current execution path of the program in a fully automatic manner. In this talk, we present a novel approach in which data-oriented and control-oriented properties may be stated in a single formalism amenable to both static and dynamic verification techniques. The specification language we present to achieve this that of ppDATEs, which enhances the control-oriented property language of DATEs, with data-oriented pre/postconditions. For runtime verification of ppDATE specifications, the language is translated into a DATE. We give a formal semantics to ppDATEs, which we use to prove the correctness of our translation from ppDATEs to DATEs. We show how ppDATE specifications can be analysed using a combination of the deductive theorem prover KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY first partially proves the data-oriented part of the specification, simplifying the specification which is then passed on to LARVA to check at runtime for the remaining parts of the specification including the control-oriented aspects. We show the applicability of our approach on two case studies.

The research area of formal methods has made enormous progress in the last 20 years, and many tools exist to apply formal methods to practical problems. Unfortunately, many of these tools are difficult to find and install, and often they are not executable due to missing installation requirements. The findability and wide adoption of tools, and the reproducibility of research results, could be improved if all major tools for formal methods were conserved and documented in a central repository of tools for formal methods (cf. FAIR principles).

This paper describes a solution to this problem: Collect and maintain essential data about tools for formal methods in a central repository, called FM-Tools, which is available at https://gitlab.com/sosy-lab/benchmarking/fm-tools. The repository contains metadata, such as which tools are available, which versions are advertized for each tool, and what command-line arguments to use for default usage. The actual tool executables are stored in tool archives at Zenodo, and for technically deep documentation, references point to archived publications or project web sites. Two communities, which are concerned with software verification and testing, already adopted the FM-Tools repository for their comparative evaluations.

Interoperability between deductive program verification tools is a well-recognized long-standing challenge. In this paper we propose a solution for a well-delineated aspect of this challenge, namely the exchange of abstract contracts for possibly stateful interfaces that represent modularity boundaries. Interoperability across tools, specification paradigms, and programming languages is achieved by focusing on abstract implementation-independent behavioral models. The approach, called Contract-LIB in reminiscence of the widely-successful SMT-LIB format, aims to standardize the language over which such contracts are formulated and provides clear guidance on its integration with established methods to connect high-level specifications with code-level data structures. We demonstrate the ideas with examples, define syntax and semantics, and discuss the rationale behind key design decisions.

This talk presents an extension of the Why3 tool to enable proofs by induction on instances of inductive predicates. It consists of a new pattern matching construction to analyze the form of such a derivation, on the one hand, and a new notion of variant to justify the termination of a recursive function that proceeds according to the size of a derivation, on the other hand. We show how this extension can be implemented conservatively, with almost no changes to Why3’s verification condition generator.

In this talk we present two languages for the representation of formal verification problems of infinite-state systems, called VMT and K2. VMT stands for Verification Modulo Theories, and is an extension of SMT-LIB for the representation of symbolic transition systems and properties over them, expressed either as invariants (must hold for all reachable states) or as more general properties in Linear Temporal Logic (LTL). VMT was designed for ease of use and to facilitate interoperability among model checking tools operating over symbolic transition systems, possibly using background theories for representing infinite-state systems. More information is available at https://vmt-lib.fbk.eu/. Also the K2 language is conceptually an extension of SMT-LIB; unlike VMT, however, K2 allows to represent imperative programs with multiple procedures. The language, which is the input format of the Kratos2 symbolic model checker, has been used successfully in different research and technology transfer projects with industrial partners as a simple but powerful intermediate language for verification. More information is available at https://kratos.fbk.eu/.

We discuss the possibility to use deductive verification tools for validating correctness witnesses. Perhaps, surprisingly, the annotations provided by automatic verifiers are often not sufficient for deductive verifiers. In this talk we identify five challenges: inductiveness, function contracts, expressiveness of expressions, gotos, and undefined behavior.

Software model checking and deductive software verification have complementary strengths and weaknesses: software model checkers are more straight-forward to use, as they analyze the program without user input; but they do not yet support complicated data structures and expressive specifications. In contrast, deductive verifiers can verify expressive specifications and complex data structures modularly, but they require the user to specify the program behavior in detail, which is a time-consuming process. Due to their differing nature, the two approaches usually remain separate. However, for industrial usage, one requires both: ease of use as well as expressiveness. Therefore, we present AutoSV-Annotator, a toolchain that integrates the two approaches for C programs. The toolchain allows a user to iteratively refine the deductive annotations in a C program, calling a model checker to supplement the annotations at each iteration, guided by the already existing annotations. We show that our tool is able to annotate and prove many tasks from the SV-Benchmarks set. Our results show that the two strategies can indeed benefit from each other.

In this talk, I present two application areas for information exchange, test-case generation and cooperation in verificaton. I start to describe how I exchange information for test-case generation with CoVeriTest, a cooperative test-case generator based on the configurable program analysis framework CPAchecker. After a brief reminder on test-case generation with verifiers, I present the circular composition used by CPAchecker and give ideas on how information exchanged on test goals but also the explored state space. Thereafter, I continue discussing general application scenarios and concrete approaches for exchanging predicate maps, CPAchecker’s format to specify the abstraction level of CPAchecker’s predicate analysis, i.e., which predicates to use where. I give an overview of producer and consumers of predicate maps and provide an idea how to exchange information between predicate and value analysis. On the one hand, I sketch how to extract information from predicate maps for value analysis, in particular to derive the relevant variables to track. On the other hand, I indicate how to use information from the value analysis to generate predicate maps. I conclude the talk with the lessons learnt from the presented exchange approaches.

SMT-LIB is a widely-used format for specification of first-order formulas over various logical theories, used by a majority of current state-of-the-art SMT solvers. In this talk, I provide a high-level overview of the format with focus on the exchange of information between software verifiers. The talk also introduces several concepts, such as annotation mechanism, that are used by various software-verification languages based on SMT.

In the Frama-C ecosystem, tool collaboration is often based on ACSL annotations. Various kinds of more complex properties are translated into basic ACSL annotations that can then be verified using different tools. Examples of properties include relational properties, temporal logic properties, test objectives, etc. In this talk we show how global (high-level) properties are specified and verified using the MetAcsl plugin of Frama-C. Such properties include security properties (isolation, confidentiality, integrity) and are highly relevant for security certification. This approach was successfully used by Thales to formally verify its JavaCard Virtual Machine for the highest level of security certification (EAL7) of Common Criteria.

There are many approaches for automated software verification, but they are either imprecise, do not scale well to large systems, or do not sufficiently leverage parallelization. We propose an approach to decompose one large verification task into multiple smaller, connected verification tasks, based on blocks in the program control flow. For each block, summaries (block contracts) are computed – based on independent, distributed, continuous refinement by communication between the blocks. The approach iteratively synthesizes preconditions to assume at the block entry (computed from postconditions received from block predecessors, i.e., which program states reach this block) and violation conditions to check at the block exit (computed from violation conditions received from block successors, i.e., which program states lead to a specification violation). This separation of concerns leads to an architecture in which blocks can be analyzed in parallel, as separate verification problems. Whenever new information is available from other blocks, the verification can decide to restart with this new information. We realize our approach on the basis of configurable program analysis and implement it for the verification of C programs in the widely used verifier CPAchecker.

Knowing which properties to specify and subsequently verify is one of the biggest bottlenecks in the use of Formal Methods [1]. Requirements are often written in natural-language, which can be ambiguous and is not generally amenable to formal verification. As a result, requirements elicitation and formalisation becomes even more important for understanding what to specify and verify.

Tools such as NASA’s Formal Requirements Elicitation Tool (FRET) have been developed to bridge the gap between natural-language requirements and the logics normally used for formal specification [2]. FRET provides a structured natural-language, called FRETISH, from which temporal logic specifications and other verification conditions can be derived. FRET has been used in many use cases to support both elicitation and formalisation of requirements. The case studies that we report on are an aircraft engine software controller, a mechanical lung ventilator, a rover carrying out an inspection task and an algorithm for autonomously grasping spent rocket stages. We discuss how the FRETISH requirements were elicited and subsequently used for specifying properties to be verified in various formal methods (model-checking, theorem proving and runtime verification approaches) encouraging a framework for interoperability.

The overarching aim of each of these case studies was different. Specifically, in the aircraft engine controller we focused our efforts on eliciting and formalising requirements in conversation with an industrial partner (Collins Aerospace) [3]. In the mechanical lung ventilator we formalised requirements that were supplied in the ABZ case study documentation with a view to developing a formal model of the system in Event-B [4]. For the inspection rover [5], the integration of various verification artefacts into an assurance case were explored, with a hazard analysis used to define the requirements that were formalised in FRET and subsequently verified against models of the system using CoCoSim and Event-B. In the autonomous grasping case study [6], the authors modelled the code of the system using Dafny, and generated a suite of runtime monitors using ROSMonitoring that were able to identify requirement violations at run time.

Tools like FRET are invaluable when communicating with engineers and developers both in academia and industry. This was evidenced by the aircraft engine controller and autonomous grasping case studies. In both, FRET’s diagrammatic and natural-language semantics helped case study providers to consider their system from different perspectives. This undoubtedly provided a bridge for these developers, providing traceability from natural-language to formalised requirements and verification conditions. This approach to demonstrating formal methods in a user-friendly way that leverages existing requirements engineering approaches encouraged our collaborators to consider using similar formal tools in the future.

Throughout these case studies, we used FRET not only as an elicitation/formalisation tool but also as a way to manage the requirements that we were defining. We used the support that FRET provides for defining parent-child relationships between requirements, which allowed us to group related requirements together. Currently this parent-child link in FRET is informal in the sense that the user can assign a parent to a requirement without any formal/automatic checks that the requirements are related in some way. In future FRET developments it may be useful to formalise this relationship to allow the user to gradually refine requirements and provide a way to verify the traceability that we have documented between them.

In these case studies, some of the integration was via existing tool-supported translations (FRET to CoCoSpec) but the others were manual translations (FRET to Event-B, Dafny and ROSMonitoring). In the future, we hope that we can provide a more logically-founded and systematic approach to integrating these formal methods. Mathematical frameworks like UTP [7] or institution theory [8] may have roles to play here. However, less formal approaches will also be beneficial including the definition of workflows to combine and use various methods alongside one another.

This work was partially supported by the Royal Academy of Engineering and EPSRC grant EP/Y001532/1, as well as Maynooth University’s Hume Doctoral Award. We thank our co-authors and collaborators on each of the case studies: Stylianos Basagiannis, Georgios Giantamidis, Vassilios Tsachouridis, Hamza Bourbouh, Anastasia Mavridou, Irfan Sljivo, Guillaume Brat, Louise Dennis, Michael Fisher, Nikos Mavrakis, Angelo Ferrando, Yang Gao and Clare Dixon.

The breakout group consisted mainly of developers of automatic software verification tools. The group formulated the following answers to questions given by organizers.

What do we want to achieve with the exchange formats?

The group wants to support the cooperation between (static and dynamic) verifiers and/or program analyses (that can provide, e.g., points-to information). It should also facilitate incremental verification, validation of verification results, human/AI interaction with verification tools, and support human reasoning about the program and found property violations.

Which objects do we want to exchange?

The group came up with the following objects: invariants (including object invariants and transition invariants), useful ghost code, abstract reachability graphs, precision sufficient to prove the task, function contracts/summaries, error conditions, ranking functions, abstract contracts (independent of the implementation), assumptions for verifiers, verification sub-tasks (that were not proven yet), memory-specific information (e.g., shape graphs), information about synchronization between threads (e.g., execution graphs or lock order), sets of specific program paths (e.g., abstract counterexamples), and meta-information about the provenance of the presented objects.

What are suitable formats to use for the exchange?

Besides the formats that are already widely used by the community (C programs, witness formats), the group suggested using (E-)ACSL and introducing specific predicates to describe some of the objects identified above. The group also discussed whether the information retrieval should be static or query-based and whether the information should be exchanged within the program (internally) or aside (externally). Here the group did not agree on answers as each option has its pros and cons.

This breakout group had participants that are working on deductive verifiers. The discussion concentrated mainly on exchange between deductive verification tools. We started by discussing how interoperability involving deductive verifiers could be good. Concrete examples where heterogeneous verification, where different tools target different properties, validation and cross-checking of verification results, and combinations with automatic tools that could be used first to resolve the basic properties, or to infer specifications.

We then discussed what would be the appropriate level of exchange. One obvious option is to exchange concrete examples, i.e., programs with specifications. Exchanging intermediate verification results would be interesting, but also much more challenging. One important candidate is the exchange of axiomatisations of data structures and logical theories, that are used in specifications, possibly based on format inspired by SMT-LIB.

Finally, we concluded the discussion by identifying areas where already some exchange is happening between deductive verifiers, such as ContractLib, and the language constructs for which exchange could take place, such as well-encapsulated objects, lemmas etc.

In a second session, the breakout group continued by identifying a list of concrete short-term actions that could be taken to experiment with information exchange: sharing axiomatisations, work on a common example together, and organise a hackathon/specathon, to make progress on the examples, share examples of verified programs, and add tools to FM-Tools.

In the long term, we believe that these actions should lead to support for specificaton exchange, annotation exchange and proof exchange. We also identified a concrete list of semantical issues that we would have to agree upon to enable this.

The state of the art in software verification is to use programming languages like C and Java, possibly annotated using ACSL, JML, and other annotation languages, to describe the verification tasks. The two breakout sessions discussed the need to exchange verification tasks and the motivation to create a new, community-based, intermediate language (IL) that is easy to support and process by tools. The requirements for the language are as follows: The IL should

1. (a)

   have a formal semantics, such that comparative evaluations of verification algorithms does not depend on interpretations, and the same should hold for witness validation,

2. (b)

   support interoperability, such that frontends and backends are exchangable,

3. (c)

   support verification and witness validation by transformation,

4. (d)

   be independent from the higher-level input language (such as C and Java) and independent from verification technology used in the backend,

5. (e)

   retain more structure than MoXI, VMT, and CHC (control flow, procedures, sequential composition, …) to express tasks before encoding to verification conditions by a particular approach,

6. (f)

   be based on well-understood programming concepts and consolidate existing languages in that spectrum (e.g., Boogie, Why3, Viper),

7. (g)

   support witness validation that is compilable to a simple first-order check (i.e., SMT) without further inference, for all properties, and

8. (h)

   appeal to use-cases in both software model checking and deductive verification.

The objects to be exchanged by the language shall be (1) programs, (2) properties, and (3) witnesses (counterexamples and invariants). The group suggests that the new IL should be based on a text format (not binary) and use a well-known base syntax (e.g., Lisp-based). As a concrete outcome, it was agreed that the language would be defined before autumn 2025 and that a track for the language shall be established by the SV-COMP competition organizers.

A verification task is a program and a (correctness) specification. The purpose of decomposition is to divide a verification task into several subtasks which can be given to (different) software verifiers for solving them. The verifier’s results then at the end need to be combined. Thus, we do not just need decomposition, but also merging of results (for which we however did not have time in the discussion).

We basically identified two sorts of decomposition:

Based on program structure

Decomposition based on program structure might split programs on branches or along paths. We decided to not discuss this longer as there are already a number of proposals around.

Based on partial results

The second sort of decomposition we considered is the one based on a partial results, i.e., one verifier has already inspected the verification task and has obtained some partial information about it. This partial information might have come along because of a non-finished (full) proof attempt or as a result of a specific query (e.g., “give me all points-to information”).

As sorts of partial results we identified (a) conditions (as in Conditional Model Checking), (b) annotated Control-Flow-Graphs/Automata (this is what e.g. the verifier Goblint could produce) or (c) specific assumptions under which the verification has succeeded (e.g., knowledge about no non-null pointers or predicates about input variables). Potential formats of such assumptions have then been further discussed in another breakout group.

Automated and deductive verifiers perform well for different challenges. This motivates different methods of cooperation, which often require the sharing of (partial) verification results. However, no widely adopted exchange format between automated and deductive verifiers exists. The working group on exchange of partial verification results focused on three aspects of a successful exchange format:

(1) The type of information that may be exchanged.

Most notably:

• $\mathrm{■}$

  Local or global assumptions that the verifier assumed;

• $\mathrm{■}$

  invariants of various types: global invariants, location-bound invariants, loop invariants, object invariants, and resource invariants; and

• $\mathrm{■}$

  properties that were established through the analysis, such as safety of assertions or nullability.

(2) Existing related formats that serve as examples of information exchange in verification.

For example the Software Witness 2.0 format and (E-)ACSL. In this context the working group also discussed various pitfalls in exchange formats: undefined behavior in the expression language and how to precisely define elements and corresponding locations tool-independently.

(3)

​The terminology to use and biases in data representation that may be introduced through certain terminology. For example, the terms assumed (compared to assert) and asserted (compared to assume) express that the information is not instructions for a potential consumer, but that it is a description of the performed work and established truths; independent of the consumer’s use case.

Going forward, we propose a wider discussion on the above concepts and ideas to establish a consumer-independent exchange format for partial verification results.

In this breakout group, we discussed how fully automatic software verifiers could be combined with deductive verifiers. We first discussed several ongoing efforts in this direction. There are several ways in which the combination can work: deductive verifiers can prove some parts that are hard for automated software verifiers, software verifiers can prove dedicated properties that are useful for the deductive verifiers. We can also use the combination to speed up the overall verification process.

One particular challenge is that deductive verifiers often uses specifications with quantifiers. Not all software verifiers can reason about those, but there are several tricks to work around this, e.g., by encoding the quantified variable as a non-deterministic variable, but this encoding hinders the exchange.

We agreed on several follow-up actions, in particular to look at some concrete examples and look what could be achieved. We also intend to collect the existing approaches for integration in a joint document, so everybody could study them. Eventually, we plan to organise some online events to discuss the experiences with some of these concrete examples.

The group went through (a part of) the list of objects for exchange between verification tools identified by Wednesday’s breakout group of the software model checking community (see Section 4.1). Using that list, we suggested further extensions of the witness format 2.0, in particular more general ghost code, modifies clause in function contracts, and support of a fragment of ACSL.

In the second part of the session, the group focused on designing a format for exchanging precision (i.e., used predicates and relevant variables) that was used during the verification run. We agreed on the objects that should represent the precision: side-effect-free and terminating C expressions together with their scope (global, local, or a particular function). We also decided to use YAML and adopt some parts of the witness format 2.0. Finally, we have formulated some action items aiming to establish the precision exchange format.