Correctness Witnesses with Function Contracts

TL;DR

This paper extends software verification witnesses to include function contracts, enabling more comprehensive correctness arguments and better tool interoperability.

Contribution

It introduces an extension to the current witness format 2.0 to support function contracts with features inspired by ACSL.

Findings

Supports export of richer verification information

Enables exchange of function contract data between tools

Improves expressiveness of correctness witnesses

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.