MutDafny: A Mutation-Based Approach to Assess Dafny Specifications

• URL: http://arxiv.org/abs/2511.15403v1
• Date: Wed, 19 Nov 2025 12:58:06 GMT
• Title: MutDafny: A Mutation-Based Approach to Assess Dafny Specifications
• Authors: Isabel Amaral, Alexandra Mendes, José Campos,
• Abstract summary: We present MutDafny, a tool that increases the reliability of Dafny specifications by automatically signaling potential weaknesses.<n>We analyze mutation operators from popular tools, identifying the ones applicable to Dafny.<n>We evaluate MutDafny's effectiveness and efficiency in a dataset of 794 real-world Dafny programs.
• Score: 46.0054630008219
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This paper explores the use of mutation testing to reveal weaknesses in formal specifications written in Dafny. In verification-aware programming languages, such as Dafny, despite their critical role, specifications are as prone to errors as implementations. Flaws in specs can result in formally verified programs that deviate from the intended behavior. We present MutDafny, a tool that increases the reliability of Dafny specifications by automatically signaling potential weaknesses. Using a mutation testing approach, we introduce faults (mutations) into the code and rely on formal specifications for detecting them. If a program with a mutant verifies, this may indicate a weakness in the specification. We extensively analyze mutation operators from popular tools, identifying the ones applicable to Dafny. In addition, we synthesize new operators tailored for Dafny from bugfix commits in publicly available Dafny projects on GitHub. Drawing from both, we equipped our tool with a total of 32 mutation operators. We evaluate MutDafny's effectiveness and efficiency in a dataset of 794 real-world Dafny programs and we manually analyze a subset of the resulting undetected mutants, identifying five weak real-world specifications (on average, one at every 241 lines of code) that would benefit from strengthening.

Related papers

• 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)
• InFi-Check: Interpretable and Fine-Grained Fact-Checking of LLMs [48.98720183285795]
  InFi-Check is a framework for interpretable and fine-grained fact-checking of large language models.<n>InFi-Checker provides supporting evidence, classify fine-grained error types, and produce justifications along with corrections.<n>Experiments show that InFi-Checker achieves state-of-the-art performance on InFi-Check-FG.
  arXiv  Detail & Related papers  (2026-01-10T20:00:17Z)
• Probing Pre-trained Language Models on Code Changes: Insights from ReDef, a High-Confidence Just-in-Time Defect Prediction Dataset [0.0]
  We present ReDef, a high-confidence benchmark of function-level modifications curated from 22 large-scale C/C++ projects.<n>Defective cases are anchored by revert commits, while clean cases are validated through post-hoc history checks.<n>This pipeline yields 3,164 defective and 10,268 clean modifications, offering substantially more reliable labels than prior existing resources.
  arXiv  Detail & Related papers  (2025-09-11T07:07:11Z)
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
  We present an APR tool for Dafny that uses formal specifications as oracles for fault localization and repair.<n>We localize faults through a series of steps, which include using Hoare logic to determine the state of each statement within the program.<n>Our tool achieves 89.6% fault localization coverage and GPT-4o mini yields the highest repair success rate of 74.18%.
  arXiv  Detail & Related papers  (2025-07-04T15:36:12Z)
• COIN: Uncertainty-Guarding Selective Question Answering for Foundation Models with Provable Risk Guarantees [51.5976496056012]
  COIN is an uncertainty-guarding selection framework that calibrates statistically valid thresholds to filter a single generated answer per question.<n>COIN estimates the empirical error rate on a calibration set and applies confidence interval methods to establish a high-probability upper bound on the true error rate.<n>We demonstrate COIN's robustness in risk control, strong test-time power in retaining admissible answers, and predictive efficiency under limited calibration data.
  arXiv  Detail & Related papers  (2025-06-25T07:04:49Z)
• A Formally Verified Robustness Certifier for Neural Networks (Extended Version) [0.0]
  Neural networks are susceptible to minor perturbations in input that cause them to misclassify.<n>Globally-robust neural networks employ a function to certify that the classification of an input cannot be altered by such a perturbation.<n>We describe the program, its specifications, and the important design decisions taken for its implementation and verification.
  arXiv  Detail & Related papers  (2025-05-11T12:05:14Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a framework that overcomes the lack of human-written snippets to enable automated proof generation of Rust code.<n> SAFE re-purposes the large number of synthesized incorrect proofs to train the self-ging capability of the fine-tuned models.<n>We achieve a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)
• Automated Software Vulnerability Static Code Analysis Using Generative Pre-Trained Transformer Models [0.8192907805418583]
  Generative Pre-Trained Transformer models have been shown to be surprisingly effective at a variety of natural language processing tasks. We evaluate the effectiveness of open source GPT models for the task of automatic identification of the presence of vulnerable code syntax.
  arXiv  Detail & Related papers  (2024-07-31T23:33:26Z)
• FineWAVE: Fine-Grained Warning Verification of Bugs for Automated Static Analysis Tools [18.927121513404924]
  Automated Static Analysis Tools (ASATs) have evolved over time to assist in detecting bugs. Previous research efforts have explored learning-based methods to validate the reported warnings. We propose FineWAVE, a learning-based approach that verifies bug-sensitive warnings at a fine-grained granularity.
  arXiv  Detail & Related papers  (2024-03-24T06:21:35Z)

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.