AutoDeduct: A Tool for Automated Deductive Verification of C Code

• URL: http://arxiv.org/abs/2501.10889v1
• Date: Sat, 18 Jan 2025 22:00:43 GMT
• Title: AutoDeduct: A Tool for Automated Deductive Verification of C Code
• Abstract summary: 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.
• Score: 0.3518504468878697
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• 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.

Related papers

• Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code [0.5296470528744145]
  Non-functional requirements, such as restrictions on control flow and data flow, are important for embedded systems safety.<n>We propose an interface specification contract language for C modules.<n>We report on two case studies on safety-critical C code using software in Scania trucks.
  arXiv  Detail & Related papers  (2026-05-19T21:12:45Z)
• Combining Mechanical and Agentic Specification Inference for Move [2.8693521708495684]
  We describe a specification inference tool for the Move Prover.<n>It combines a weakest-precondition analysis over Move bytecode with an agentic coding CLI such as Claude Code.<n>The tool has been applied to a corpus of canonical Move code.
  arXiv  Detail & Related papers  (2026-05-11T05:30:25Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  Existing benchmarks test only individual languages/tools, so the performance numbers are not directly comparable.<n>We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean.
  arXiv  Detail & Related papers  (2026-02-10T06:58:26Z)
• 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)
• 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)
• Do Large Language Models Respect Contracts? Evaluating and Enforcing Contract-Adherence in Code Generation [11.445615378917578]
  PACT is a program assessment and contract-adherence evaluation framework.<n>It provides a comprehensive test-suite corpus focused on contract violations.<n>It enables a systematic analysis of code generation under varied prompting conditions.
  arXiv  Detail & Related papers  (2025-10-14T01:12:37Z)
• Scaling Code-Assisted Chain-of-Thoughts and Instructions for Model Reasoning [65.20602712957725]
  Caco is a novel framework that automates the synthesis of high-quality, verifiable, and diverse instruction-CoT reasoning data.<n>Our work establishes a paradigm for building self-sustaining, trustworthy reasoning systems without human intervention.
  arXiv  Detail & Related papers  (2025-10-05T07:59:24Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  The paper introduces forward and backward constraints generation to improve the instruction-following capabilities of Code LLMs.<n>The authors present IFEvalCode, a multilingual benchmark comprising 1.6K test samples across seven programming languages.
  arXiv  Detail & Related papers  (2025-07-30T08:08:48Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• C*: Unifying Programming and Verification in C [15.531046191957529]
  C* is a proof-integrated language design for C programming. It enables real-time verification by allowing programmers to embed proof-code blocks alongside implementation code. C* unifies implementation and proof code development by using C as the common language.
  arXiv  Detail & Related papers  (2025-04-03T03:22: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)
• Correctness Witnesses with Function Contracts [0.1499944454332829]
  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.
  arXiv  Detail & Related papers  (2025-01-21T17:27:59Z)
• VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models [1.6249267147413524]
  VECOGEN is a novel tool that combines large language models with formal verification to automate the generation of formally verified C programs. VECOGEN takes a formal specification in/ISO C Specification Language, a natural language specification, and a set of test cases to attempt to generate a verified program.
  arXiv  Detail & Related papers  (2024-11-28T17:12:21Z)
• 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)
• SEP: Self-Enhanced Prompt Tuning for Visual-Language Model [93.94454894142413]
  We introduce a novel approach named Self-Enhanced Prompt Tuning (SEP) SEP explicitly incorporates discriminative prior knowledge to enhance both textual-level and visual-level embeddings. Comprehensive evaluations across various benchmarks and tasks confirm SEP's efficacy in prompt tuning.
  arXiv  Detail & Related papers  (2024-05-24T13:35:56Z)
• CELA: Cost-Efficient Language Model Alignment for CTR Prediction [70.65910069412944]
  Click-Through Rate (CTR) prediction holds a paramount position in recommender systems.<n>Recent efforts have sought to mitigate these challenges by integrating Pre-trained Language Models (PLMs)<n>We propose textbfCost-textbfEfficient textbfLanguage Model textbfAlignment (textbfCELA) for CTR prediction.
  arXiv  Detail & Related papers  (2024-05-17T07:43:25Z)
• General Point Model with Autoencoding and Autoregressive [55.051626723729896]
  We propose a General Point Model which seamlessly integrates autoencoding and autoregressive tasks in point cloud transformer. This model is versatile, allowing fine-tuning for downstream point cloud representation tasks, as well as unconditional and conditional generation tasks.
  arXiv  Detail & Related papers  (2023-10-25T06:08:24Z)
• Generalizable Chain-of-Thought Prompting in Mixed-task Scenarios with Large Language Models [68.05046964022844]
  Large language models (LLMs) have unveiled remarkable reasoning capabilities by exploiting chain-of-thought (CoT) prompting. We propose GeM-CoT, a Generalizable CoT prompting mechanism in Mixed-task scenarios where the type of input questions is unknown. With this technical design, GeM-CoT simultaneously enjoys superior generalization capabilities and remarkable performances on 10 public reasoning tasks and 23 BBH tasks.
  arXiv  Detail & Related papers  (2023-10-10T15:10:03Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  In deductive verification and software model checking, dealing with certain specification language constructs can be problematic. We propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation.
  arXiv  Detail & Related papers  (2023-05-26T14:55:35Z)
• Verified Reversible Programming for Verified Lossless Compression [11.020543186794459]
  Lossless compression implementations typically contain two programs, an encoder and a decoder, which are required to be inverse to one another. We observe that a significant class of compression methods, based on asymmetric numeral systems (ANS), have shared structure between the encoder and decoder. We have implemented a small reversible language, embedded in Agda, which we call 'Flipper'
  arXiv  Detail & Related papers  (2022-11-02T16:39:41Z)
• Binding Language Models in Symbolic Languages [146.3027328556881]
  Binder is a training-free neural-symbolic framework that maps the task input to a program. In the parsing stage, Codex is able to identify the part of the task input that cannot be answerable by the original programming language. In the execution stage, Codex can perform versatile functionalities given proper prompts in the API calls.
  arXiv  Detail & Related papers  (2022-10-06T12:55:17Z)
• CodeT5: Identifier-aware Unified Pre-trained Encoder-Decoder Models for Code Understanding and Generation [36.47905744758698]
  We present CodeT5, a unified pre-trained encoder-decoder Transformer model that better leverages the code semantics conveyed from the developer-assigned identifiers. Our model employs a unified framework to seamlessly support both code understanding and generation tasks and allows for multi-task learning.
  arXiv  Detail & Related papers  (2021-09-02T12:21:06Z)

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.