AutoDeduct: A Tool for Automated Deductive Verification of C Code

TL;DR

Deductive verification of C code imposes a heavy manual annotation burden. AutoDeduct provides an automated pipeline built on Frama-C that infers functional and auxiliary ACSL contracts given an entry-point contract, enabling deductive verification with the WP plugin. It combines Horn-clause model checking (TriCera) for functional inference and Eva-based abstract interpretation for auxiliary annotations, producing a fully annotated program. Evaluation on an industrially inspired module (~$ca. 1400$ LOC) demonstrates rapid verification and automated contract generation, highlighting the approach's practical viability for embedded software.

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.

Figures (3)

• Figure 1: Example program with a main function and three helper functions, where only the main function is given a contract.
• Figure 2: Architecture of AutoDeduct
• Figure 3: Inferred contracts for the program and