2025/01/21 by Matthias Heizmann, Heizmann, Matthias, Dominik Klumpp +5
Economics, Econometrics and Finance · Health Professions · #FOS: Computer and information sciences #Law, Economics, and Judicial Systems #Medical Malpractice and Liability Issues #Programming Languages (cs.PL) #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.2501.12313
openalex publication_date 2025/01/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.