AutoDeduct: A Tool for Automated Deductive Verification of C Code
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910789704613888 |
|---|---|
| author | Amilon, Jesper Gurov, Dilian Lidström, Christian Nyberg, Mattias Ung, Gustav Wingbrant, Ola |
| author_facet | Amilon, Jesper Gurov, Dilian Lidström, Christian Nyberg, Mattias Ung, Gustav Wingbrant, Ola |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_10889 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | AutoDeduct: A Tool for Automated Deductive Verification of C Code Amilon, Jesper Gurov, Dilian Lidström, Christian Nyberg, Mattias Ung, Gustav Wingbrant, Ola Logic in Computer Science Software Engineering 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. |
| title | AutoDeduct: A Tool for Automated Deductive Verification of C Code |
| topic | Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2501.10889 |