Correctness Witnesses with Function Contracts

• URL: http://arxiv.org/abs/2501.12313v1
• Date: Tue, 21 Jan 2025 17:27:59 GMT
• Title: Correctness Witnesses with Function Contracts
• Abstract summary: We propose an extension to the existing witness format 2.0 to allow for the specification of function contracts.<n>This allows for the export of more information from tools and for the exchange of information with tools that require function contracts.
• Score: 0.1499944454332829
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles [3.4742046772246837]
  In experiments on 110 Dafny programs, a multimodel approach combining Claude Opus 4.5 and GPT-5.2 generated correct annotations for 98.2% of the programs within at most 8 repair iterations.<n>A logistic regression analysis shows that proof-helper annotations contribute disproportionately to problem difficulty for current LLMs.
  arXiv  Detail & Related papers  (2026-01-19T08:56:43Z)
• SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks [2.5374060352463697]
  SV-LIB is an exchange format and intermediate language for software-verification tasks.<n>This paper presents version 1.0 of the SV-LIBformat, including its design goals, the syntax, and informal semantics.
  arXiv  Detail & Related papers  (2025-11-26T15:44:54Z)
• Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification? [1.9551668880584971]
  Large Language Models (LLMs) have shown promise in inferring formal postconditions from natural language hints.<n>We introduce NL2Contract, the task of employing LLMs to translate informal natural language into formal functional contracts.<n>We evaluate NL2Contract with different LLMs and compare it to the task of postcondition generation nl2postcond.
  arXiv  Detail & Related papers  (2025-10-14T16:37:39Z)
• Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version) [0.2446948464551684]
  This paper presents a methodology to formally verify the correctness of Stipula contracts through translation into Java code annotated with Java Modeling Language specifications.<n>As a verification backend, the deductive verification tool KeY is used.
  arXiv  Detail & Related papers  (2025-09-24T14:06:22Z)
• SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
  We introduce SolBench, a benchmark for evaluating the functional correctness of Solidity smart contracts generated by code completion models. We propose a Retrieval-Augmented Code Repair framework to verify functional correctness of smart contracts. Results show that code repair and retrieval techniques effectively enhance the correctness of smart contract completion while reducing computational costs.
  arXiv  Detail & Related papers  (2025-03-03T01:55:20Z)
• Formal verification in Solidity and Move: insights from a comparative analysis [0.40964539027092906]
  Solidity and Move are two contract languages with different designs and approaches to verification. This paper investigates how the two languages impact verification, and what is the state-of-the-art of verification tools for the two languages. Our investigation is supported by an open dataset of verification tasks performed in Certora and in the Aptos Move Prover.
  arXiv  Detail & Related papers  (2025-02-19T18:06:01Z)
• AutoDeduct: A Tool for Automated Deductive Verification of C Code [0.3518504468878697]
  We introduce the AutoDeduct toolchain, built on top of the Frama-C framework.<n>It implements a combination of techniques to automatically infer contracts for functions in C programs.<n>The current release of AutoDeduct is the first public prototype.
  arXiv  Detail & Related papers  (2025-01-18T22:00:43Z)
• COBRA: Interaction-Aware Bytecode-Level Vulnerability Detector for Smart Contracts [4.891180928768215]
  We propose COBRA, a framework that integrates semantic context and function interfaces to detect vulnerabilities in smart contracts. To infer the function signatures that are not present in signature databases, we present SRIF, which automatically learns the rules of function signatures from the smart contract bytecodes. Experimental results demonstrate that SRIF can achieve 94.76% F1-score for function signature inference.
  arXiv  Detail & Related papers  (2024-10-28T03:55:09Z)
• GenAudit: Fixing Factual Errors in Language Model Outputs with Evidence [64.95492752484171]
  We present GenAudit -- a tool intended to assist fact-checking LLM responses for document-grounded tasks. We train models to execute these tasks, and design an interactive interface to present suggested edits and evidence to users. To ensure that most errors are flagged by the system, we propose a method that can increase the error recall while minimizing impact on precision.
  arXiv  Detail & Related papers  (2024-02-19T21:45:55Z)
• Enhancing Translation Validation of Compiler Transformations with Large Language Models [5.103162976634333]
  This paper presents a framework that integrates Large Language Models (LLMs) into translation validation. We first utilize existing formal verification tools for translation validation. When formal verification tools are unable to confirm a transformation's soundness, our framework employs fine-tuned LLMs for prediction.
  arXiv  Detail & Related papers  (2024-01-30T07:24:04Z)
• An Efficient VCGen-based Modular Verification of Relational Properties [1.567576360103422]
  Deductive verification typically relies on function contracts that specify the behavior of each function for a single function call. Recent work proposed a new technique for relational property verification that relies on a verification condition generator.
  arXiv  Detail & Related papers  (2024-01-16T14:19:04Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  We present a holistic end-to-end solution for annotating the factuality of large language models (LLMs)-generated responses. We construct an open-domain document-level factuality benchmark in three-level granularity: claim, sentence and document. Preliminary experiments show that FacTool, FactScore and Perplexity are struggling to identify false claims.
  arXiv  Detail & Related papers  (2023-11-15T14:41:57Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  Recent Language Models (LMs) have shown impressive capabilities in generating texts with the knowledge internalized in parameters. We propose to verify the output and the knowledge of the knowledge-augmented LMs with a separate verifier. Our results show that the proposed verifier effectively identifies retrieval and generation errors, allowing LMs to provide more factually correct outputs.
  arXiv  Detail & Related papers  (2023-10-19T15:40:00Z)
• FacTool: Factuality Detection in Generative AI -- A Tool Augmented Framework for Multi-Task and Multi-Domain Scenarios [87.12753459582116]
  A wider range of tasks now face an increasing risk of containing factual errors when handled by generative models. We propose FacTool, a task and domain agnostic framework for detecting factual errors of texts generated by large language models.
  arXiv  Detail & Related papers  (2023-07-25T14:20:51Z)
• Give Me More Details: Improving Fact-Checking with Latent Retrieval [58.706972228039604]
  Evidence plays a crucial role in automated fact-checking. Existing fact-checking systems either assume the evidence sentences are given or use the search snippets returned by the search engine. We propose to incorporate full text from source documents as evidence and introduce two enriched datasets.
  arXiv  Detail & Related papers  (2023-05-25T15:01:19Z)
• Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
  AuditAI bridges the gap between interpretable formal verification and scalability. We show how AuditAI allows us to obtain controlled variations for verification and certified training while addressing the limitations of verifying using only pixel-space perturbations.
  arXiv  Detail & Related papers  (2021-09-25T22:53:24Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.