AutoDeduct: A Tool for Automated Deductive Verification of C Code
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.
Cite
@article{arxiv.2501.10889,
title = {AutoDeduct: A Tool for Automated Deductive Verification of C Code},
author = {Jesper Amilon and Dilian Gurov and Christian Lidström and Mattias Nyberg and Gustav Ung and Ola Wingbrant},
journal= {arXiv preprint arXiv:2501.10889},
year = {2025}
}