AutoDeduct: A Tool for Automated Deductive Verification of C Code

TL;DR

AutoDeduct is a tool that automates the inference of function contracts in C programs to facilitate deductive verification, reducing manual annotation effort and enabling verification of industrial software.

Contribution

It introduces a novel toolchain with plugins for automatic contract inference in C code, integrated with Frama-C, to streamline deductive verification processes.

Findings

Successfully infers contracts for helper functions from a given entry-point contract.

Automates a significant manual effort in deductive verification workflows.

Evaluated on an industrial software example, demonstrating practical applicability.

Abstract

Deductive verification has become a mature paradigm for the verification of industrial software. Applying deductive verification, however, requires that every function in the code base is annotated with a function contract specifying its behaviour. This introduces a large overhead of manual work. To address this challenge, we introduce the AutoDeduct toolchain, built on top of the Frama-C framework. It implements a combination of techniques to automatically infer contracts for functions in C programs, in the syntax of ACSL, the specification language of Frama-C. Contract inference in AutoDecuct is implemented as two plugins for Frama-C, each inferring different types of annotations. We assume that programs have an entry-point function already equipped with a contract, which is used in conjunction with the program source code to infer contracts for the helper functions, so that the entry-point contract can be verified. The current release of AutoDeduct is the first public prototype, which we evaluate on an example adapted from industrial software.