Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Correctness Witnesses with Function Contracts

Matthias Heizmann, Dominik Klumpp, Marian Lingsch-Rosenfeld, Frank Schüssele

TL;DR

Correctness Witnesses in SV-COMP version 2.0 lacked a mechanism to encode function contracts, limiting modular verification. The authors introduce an invariant_set extension with a new function_contract entry and support for an acsl_expression format using $\old$, $\at$, and $\result$ to express pre/post conditions and cross-state relations. This extension remains backward-compatible for verifiers and enables validation by deductive verifiers, potentially enabling full correctness certificates for many programs. Limitations include heap/pointer invariants and data abstraction, with future work proposed on extending the expression language and incorporating ghost variables.

Abstract

Software verification witnesses are a common exchange format for software verification tools. They were developed to provide arguments supporting the verification result, allowing other tools to reproduce the verification results. Correctness witnesses in the current format (version 2.0) allow only for the encoding of loop and location invariants using C expressions. This limits the correctness arguments that verifiers can express in the witness format. One particular limitation is the inability to express function contracts, which consist of a pre-condition and a post-condition for a function. We propose an extension to the existing witness format 2.0 to allow for the specification of function contracts. Our extension includes support for several features inspired by ACSL (\result, \old, \at). This allows for the export of more information from tools and for the exchange of information with tools that require function contracts.

Correctness Witnesses with Function Contracts

TL;DR

Correctness Witnesses in SV-COMP version 2.0 lacked a mechanism to encode function contracts, limiting modular verification. The authors introduce an invariant_set extension with a new function_contract entry and support for an acsl_expression format using , , and to express pre/post conditions and cross-state relations. This extension remains backward-compatible for verifiers and enables validation by deductive verifiers, potentially enabling full correctness certificates for many programs. Limitations include heap/pointer invariants and data abstraction, with future work proposed on extending the expression language and incorporating ghost variables.

Abstract

Software verification witnesses are a common exchange format for software verification tools. They were developed to provide arguments supporting the verification result, allowing other tools to reproduce the verification results. Correctness witnesses in the current format (version 2.0) allow only for the encoding of loop and location invariants using C expressions. This limits the correctness arguments that verifiers can express in the witness format. One particular limitation is the inability to express function contracts, which consist of a pre-condition and a post-condition for a function. We propose an extension to the existing witness format 2.0 to allow for the specification of function contracts. Our extension includes support for several features inspired by ACSL (\result, \old, \at). This allows for the export of more information from tools and for the exchange of information with tools that require function contracts.
Paper Structure (4 sections, 3 figures, 1 table)

This paper contains 4 sections, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Syntax
  3. Semantics
  4. Discussion

Figures (3)

  • Figure 1: C programs annotated with (relational) function contracts and (relational) invariants in ACSL.
  • Figure 2: An example program (left) and a excerpt of a correctness witness with function contracts (right)
  • Figure 3: C program (left) and corresponding witness (right), where \\ old is necessary to express the correctness of the program. The witness encodes the same information expressed in \ref{['fig:example-acsl']} as ACSL annotations.