Correctness Witnesses with Function Contracts
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915113753116672 |
|---|---|
| author | Heizmann, Matthias Klumpp, Dominik Lingsch-Rosenfeld, Marian Schüssele, Frank |
| author_facet | Heizmann, Matthias Klumpp, Dominik Lingsch-Rosenfeld, Marian Schüssele, Frank |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_12313 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Correctness Witnesses with Function Contracts Heizmann, Matthias Klumpp, Dominik Lingsch-Rosenfeld, Marian Schüssele, Frank Programming Languages Software Engineering 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. |
| title | Correctness Witnesses with Function Contracts |
| topic | Programming Languages Software Engineering |
| url | https://arxiv.org/abs/2501.12313 |